Abstract. We present an encoding for (bound) processes of the asynchronous CCS with replication into open Petri nets: ordinary Petri nets equipped with a distinguished set of open ...
We propose how to present and compute a counterexample in probabilistic LTL model checking for discrete-time Markov chains. In qualitative probabilistic model checking, we present ...
Theories identifying well-formed systems of processes—those that are free of communication errors and enjoy strong properties such as deadlock freedom—are based either on sessi...
Several programming constructs have recently been proposed with the purpose of enabling the programmer to encode declassifying information flows within a program that complies wi...
Stuttering bisimulation is a well-known behavioural equivalence that preserves CTL-X, namely CTL without the next-time operator X. Correspondingly, the stuttering simulation preord...
We present a compositional method for deriving control constraints on a network of interconnected, partially observable and partially controllable plant components. The constraint ...
Abstract. A prominent source of complexity in the verification of ad hoc network (AHN) protocols is the fact that the number of network topologies grows exponentially with the squ...
Nondeterministic weighted automata are finite automata with numerical weights on transitions. They define quantitative languages L that assign to each word w a real number L(w). ...
Krishnendu Chatterjee, Laurent Doyen, Thomas A. He...