Whereas formal verification of timed systems has become a very active field of research, the idealised mathematical semantics of timed automata cannot be faithfully implemented. Se...
Patricia Bouyer, Nicolas Markey, Pierre-Alain Reyn...
Abstract. Symbolic bisimulations were introduced as a mean to define value-passing process calculi using smaller, possibly finite labelled transition systems, equipped with symboli...
We study complexity issues related to the model-checking problem for LTL with registers (a.k.a. freeze LTL) over one-counter automata. We consider several classes of one-counter au...
Protocols for information-hiding often use randomized primitives to obfuscate the link between the observables and the information to be protected. The degree of protection provide...
Abstract. A syntactic framework called SGSOS, for defining well-behaved Markovian stochastic transition systems, is introduced by analogy to the GSOS congruence format for nondeter...
We introduce a new decidable logic for reasoning about infinite arrays of integers. The logic is in the first-order fragment and allows (1) Presburger constraints on existentially...
We consider turn-based stochastic games on infinite graphs induced by game probabilistic lossy channel systems (GPLCS), the game version of probabilistic lossy channel systems (PLC...
Parosh Aziz Abdulla, Noomene Ben Henda, Luca de Al...