We re-examine vacuity in temporal logic model checking. We note two disturbing phenomena in recent results in this area. The first indicates that not all vacuities detected in prac...
We consider message sequence charts enriched with timing constraints between pairs of events. As in the untimed setting, an infinite family of time-constrained message sequence cha...
Abstract. We consider the problem of verifying the safety of wellstructured transition systems (WSTS) with auxiliary storage. WSTSs with storage are automata that have (possibly) i...
Abstract. In this paper, we provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving...
Taolue Chen, Bas Ploeger, Jaco van de Pol, Tim A. ...
Abstract. Almost 20 years after the original conception, we revisit several fundamental questions about modal transition systems. First, we demonstrate the incompleteness of the st...
Kim Guldstrand Larsen, Ulrik Nyman, Andrzej Wasows...
It is well known that bisimulation on µ-expressions cannot be finitely axiomatised in equational logic. Complete axiomatisations such as those of Milner and Bloom/´Esik necessar...
The notion of innocent strategy was introduced by Hyland and Ong in order to capture the interactive behaviour of λ-terms and PCF programs. An innocent strategy is defined as an ...
We present a fixpoint-based algorithm for context-sensitive interprocedural kill/gen-analysis of programs with thread creation. Our algorithm is precise up to abstraction of sync...