Search

• < Previous
• 1
• Next >

---

On the Expressiveness and Complexity of ATL

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&nbsp;[&hellip;]

---

Model Checking Probabilistic Timed Automata with One or Two Clocks

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&nbsp;[&hellip;]

---

Quantified CTL: Expressiveness and Complexity

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&nbsp;[&hellip;]

---