X Liu, SA Smolka - … Programming: 25th International Colloquium, ICALP'98 …, 1998 - Springer
We present global and local algorithms for evaluating minimal fixed points of dependency graphs, a general problem in fixed-point computation and model checking. Our algorithms …
DE Long, A Browne, EM Clarke, S Jha… - … Aided Verification: 6th …, 1994 - Springer
Many automated finite-state verification procedures can be viewed as fixpoint computations over a finite lattice (typically the powerset of the set of system states). Hence, fixpoint calculi …
S Kuske, M Gogolla, R Kollmann… - International conference on …, 2002 - Springer
This paper studies the semantics of a central part of the Unified Modeling Language UML. It discusses UML class, object and state diagrams and presents a new integrated semantics …
A Browne, EM Clarke, S Jha, DE Long… - Theoretical Computer …, 1997 - Elsevier
Many automated finite-state verification procedures can be viewed as fixpoint computations over a finite lattice (typically the powerset of the set of system states). For this reason, fixpoint …
B Steffen - Science of Computer Programming, 1993 - Elsevier
The paper develops a framework that is based on the idea that modal logic provides an appropriate framework for the specification of data flow analysis (DFA) algorithms as soon …
MY Vardi, T Wilke - Logic and automata, 2008 - library.oapen.org
We review, in a unified framework, translations from five different logics—monadic second- order logic of one and two successors (S1S and S2S), linear-time temporal logic (LTL) …
H Seidl - Information Processing Letters, 1996 - Elsevier
We give an alternative proof of the result of Long et al.(1994) that nested fixpoint expressions e of alternation depth d> 1 can be evaluated over a complete lattice of height h …
We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal/spl mu/-calculus. The proof system is …
We define five increasingly comprehensive classes of infinite-state systems, called STS1-- STS5, whose state spaces have finitary structure. For four of these classes, we provide …