40 citations · 104 across the 7 of their papers we have counts for
8 papers
QCTL model-checking with QBF solvers
A. Hossain, F. Laroussinie
Quantified CTL (QCTL) extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex…
From Quantified CTL to QBF
Akash Hossain, Francois Laroussinie
QCTL extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over…
ATLsc with partial observation
François Laroussinie, Nicolas Markey, Arnaud Sangnier
Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, o…
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…
Satisfiability of ATL with strategy contexts
François Laroussinie, Nicolas Markey
Various extensions of the temporal logic ATL have recently been introduced to express rich properties of multi-agent systems. Among these, ATLsc extends ATL with strategy contexts,…
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 cert…
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 t…
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 o…