A seminal theorem by van Benthem characterises the bisimulation-invariant fragment of First Order Logic (FOL) in terms of Modal Logic. Similarly, Janin and Walukiewicz have shown that the bisimulation-invariant fragment of Monadic Second Order Logic (MSO)...

Many analysis and verifications tasks, such as static program analyses and model-checking for temporal logics, reduce to the solution of systems of equations over suitable lattices. Inspired by recent work on lattice-theoretic progress measures, we ...

We revisit Janin and Walukiewicz’s classic result on the expressive completeness of the modal mu-calculus with respect to Monadic Second Order Logic (MSO), which is where the mu-calculus corresponds precisely to the fragment of MSO that is invariant ...

Modal μ-calculus is one of the central languages of logic and verification, whose study involves notoriously complex objects: automata over infinite structures on the model-theoretical side; infinite proofs and proofs by (co)induction on the proof-...

We prove a general decomposition theorem for the modal μ-calculus L_μ in the spirit of Feferman and Vaught's theorem for disjoint unions. In particular, we show that if a structure (i.e., transition system) is composed of two substructures M₁ and M₂ plus ...

We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history-preserving bisimilarity, and fragments of the logic can be identified ...

Data-centric dynamic systems are systems where both the process controlling the dynamics and the manipulation of data are equally central. We study verification of (first-order) mu-calculus variants over relational data-centric dynamic systems, where ...

The semantics of fixed point constructions is commonly defined in terms of iteration sequences. For example, the least fixed point of a monotone operator consists of all points which eventually appear in the approximations computed iteratively. We take ...

The problem of verifying software systems that use dynamic data structures (such as linked lists, queues, or binary trees) has attracted increasing interest over the last decade. Dynamic structures are barely supported by verification techniques because ...

We study the problem of substitution of components in a composite service, especially in the setting where the substitute is composed in an asynchronous fashion. By asynchronous composition, we mean that the participants in the composition are not ...

We show that recursive programs where variables range over finite domains can be effectively and efficiently analyzed by describing the analysis algorithm using a formula in a fixed-point calculus. In contrast with programming in traditional languages, ...

In this paper we investigate the Scott continuous fragment of the modal μ -calculus. We discuss its relation with constructivity, where we call a formula constructive if its least fixpoint is always reached in at most ï steps. Our main result is a ...

Pushdown Systems (PDSs) have become an important paradigm for program analysis. Indeed, recent work has shown a deep connection between inter-procedural dataflow analysis for sequential programs and the model checking problem for PDSs. A natural ...

The quantitative @m-calculus qM@m extends the applicability of Kozen's standard @m-calculus [D. Kozen, Results on the propositional @m-calculus, Theoretical Computer Science 27 (1983) 333-354] to probabilistic systems. Subsequent to its introduction [C. ...

On-the-fly verification of concurrent finite-state systems consists in constructing and analysing their underlying state spaces in a demand-driven way. This technique is able to detect errors effectively in large systems; however, its performance can ...

In this paper we give some abstractions that preserve sublanguages of the universal part of the branching-time μ-calculus L_μ. We first extend some results by Loiseaux et al. by using a different abstraction for the universal fragments of L_μ which are ...

Model-checking is a successful technique for automatically verifying concurrent finite-state systems. When designing a model-checker, a good compromise must be made between the expressive power of the property description formalism, the complexity of ...

This paper shows that different "meta-model-checking" analyses can be conducted efficiently on a generic data structure we call a support set. Support sets may be viewed as abstract encodings of the "evidence" a model checker uses to justify the yes/no ...

We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning of a Tarskian function symbol is interpreted in an ...

An algorithm for model checking value-passing processes is presented.Processes are modeled as symbolic transition graphs with assignments. To specify properties for such processes a graphical predicate mu-calculus isintroduced.It allows arbitrary ...