28 citations · 38 across the 5 of their papers we have counts for
5 papers
A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability
Simon Busard, Charles Pecheur
Since the introduction of Alternating-time Temporal Logic (ATL), many logics have been proposed to reason about different strategic capabilities of the agents of a system. In parti…
Verification of railway interlocking - Compositional approach with OCRA
Christophe Limbree, Quentin Cappart, Charles Pecheur +1
In the railway domain, an electronic interlocking is a computerised system that controls the railway signalling components (e.g. switches or signals) in order to allow a safe opera…
Verification of railway interlocking systems
Simon Busard, Quentin Cappart, Christophe Limbrée +2
In the railway domain, an interlocking is a computerised system that controls the railway signalling objects in order to allow a safe operation of the train traffic. Each interlock…
Reasoning about Strategies under Partial Observability and Fairness Constraints
Simon Busard, Charles Pecheur, Hongyang Qu +1
A number of extensions exist for Alternating-time Temporal Logic; some of these mix strategies and partial observability but, to the best of our knowledge, no work provides a unifi…
Rich Counter-Examples for Temporal-Epistemic Logic Model Checking
Simon Busard, Charles Pecheur
Model checking verifies that a model of a system satisfies a given property, and otherwise produces a counter-example explaining the violation. The verified properties are formally…