In a seminal paper from 1985, Sistla and Clarke showed that satisfiability for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of tempora...
Michael Bauland, Thomas Schneider 0002, Henning Sc...
Desharnais, Gupta, Jagadeesan and Panangaden introduced a family of behavioural pseudometrics for probabilistic transition systems. These pseudometrics are a quantitative analogue ...
We study the complexity of satisfiability for the expressive extension ICPDL of PDL (Propositional Dynamic Logic), which admits intersection and converse as program operations. Ou...
Abstract. Logics that can reason about sets and their cardinality bounds are useful in program analysis, program verification, databases, and knowledge bases. This paper presents ...
Higher-order pushdown systems (PDSs) generalise pushdown systems through the use of higher-order stacks, that is, a nested “stack of stacks” structure. These systems may be us...
Abstract. System L is a linear λ-calculus with numbers and an iterator, which, although imposing linearity restrictions on terms, has all the computational power of G¨odel’s Sy...
We give logical characterizations of bisimulation relations for the probabilistic automata of Segala in terms of three Hennessy-Milner style logics. The three logics characterize s...
We use the framework of biorthogonality to introduce a novel semantic definition of the concept of barb (basic observable) for process calculi. We develop a uniform basic theory o...