showing 2 related works from this author
Verification of scope-dependent hierarchical state machines
2008
AbstractA hierarchical state machine (Hsm) is a finite state machine where a vertex can either expand to another hierarchical state machine (box) or be a basic vertex (node). Each node is labeled with atomic propositions. We study an extension of such model which allows atomic propositions to label also boxes (Shsm). We show that Shsms can be exponentially more succinct than Shsms and verification is in general harder by an exponential factor. We carefully establish the computational complexity of reachability, cycle detection, and model checking against general Ltl and Ctl specifications. We also discuss some natural and interesting restrictions of the considered problems for which we can …
Finite automata on timed ω-trees
2003
AbstractIn the last decade Alur and Dill introduced a model of automata on timed ω-sequences which extends the traditional models of finite automata. In this paper, we present a theory of timed ω-trees which extends both the theory of timed ω-sequences and the theory of ω-trees. The main motivation is to introduce a new way of specifying real-time systems and provide tools for studying decidability problems in related fields. We focus on the decision problems and their applications in system verification and synthesis.