3 results
Francois Laroussinie ; Nicolas Markey ; Ghassan Oreiby.
ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. In this paper, we first precisely characterize the complexity of ATL […]
Published on May 15, 2008
Marcin Jurdzinski ; Francois Laroussinie ; Jeremy Sproston.
Probabilistic timed automata are an extension of timed automata with discrete probability distributions. We consider model-checking algorithms for the subclasses of probabilistic timed automata which have one or two clocks. Firstly, we show that PCTL probabilistic model-checking problems (such as […]
Published on September 26, 2008
François Laroussinie ; Nicolas Markey.
While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its […]
Published on December 25, 2014