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 One-clock Priced Timed Automata

Patricia Bouyer ; Kim G. Larsen ; Nicolas Markey.

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities.&nbsp;[&hellip;]

---

Language Preservation Problems in Parametric Timed Automata

Étienne André ; Didier Lime ; Nicolas Markey.

Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter&nbsp;[&hellip;]

---