Modal and mixed transition systems are formalisms that allow mixing of over- and under-approximation in a single specification. We show EXPTIME-completeness of three fundamental decision problems for such specifications: whether a set of modal or mixed ...

Keywords: EXPTIME-completeness, decision problem, mixed transition system, modal transition system

Reachability analysis asks whether a system can evolve from legitimate initial states to unsafe states. It is thus a fundamental tool in the validation of computational systems—be they software, hardware, or a combination thereof. We recall a ...

Keywords: Abstraction, Asynchronous systems, Bit-vector arithmetic, Bounded reachability, Decision diagrams, Decision problems, Memory models

We propose a pattern for designing algorithms that run in polynomial time by construction and under-approximate the winning regions of both players in parity games. This approximation is achieved by the interaction of finitely many aspects governed by ...

Keywords: abstraction, algorithms, computational complexity, parity games

Abstractions of programs are traditionally over-approximations and have proved to be useful for the verification of safety properties. They are presently perceived as being useless for the falsification of safety properties, i.e. showing that program ...

Keywords: falsification, games, software verification

We present Hintikka games for formulae of the probabilistic temporal logic PCTL and countable labeled Markovchains as models, giving an operational account of the denotational semantics of PCTL on such models. Winning strategies have a decent degree ...

Many applications, for instance the MS .NET Global Assembly Cache (GAC), are naturally expressed as 3-valued models where an additional third truth value models uncertainty or under-specification. An example of under-specification is that a component ...

Keywords: Consistency checking, Hybrid logic, Model checking, Satisfiability

It is difficult to develop and manage large, multi-author access control policies without a means to compose larger policies from smaller ones. Ideally, an access-control policy language will have a small set of simple policy combinators that allow for ...

Keywords: access control, policy languages, Belnap logic, policy analysis

In defining large, complex access control policies, one would like to compose sub-policies, perhaps authored by different organizations, into a single global policy. Existing policy composition approaches tend to be ad-hoc, and do not explain whether ...

Keywords: access-control policy languages, bilattices, multi-valued logic

Model checking is a particular approach to property verification of systems. One describes a system in a mathematical model, expresses the properties one wishes to verify for the system in a formal language, and then checks whether the model satisfies ...

Keywords: Feature integration, Game semantics, Incremental design, Model checking, Refinement checking, Slicing, Temporal logic

We generalize the familiar semantics for probabilistic computation tree logic from finite-state to infinite-state labelled Markov chains such that formulas are interpreted as measurable sets. Then we show how to synthesize finite-state abstractions which ...

Keywords: Markov chain, abstraction, optimality, probabilistic model checking