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;]

---