Search

• < Previous
• 1
• Next >

---

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

---

Counting CTL

François Laroussinie ; Antoine Meyer ; Eudes Petonnet.

This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints,&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;]

---

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

---