Hausmann, Daniel 
ORCID: 0000-0002-0935-8602, Humml, Merlin, Prucker, Simon and Schröder, Lutz
(2026)
Efficient Model Checking for the Alternating-Time $$\mu $$-Calculus via Effectivity Frames
In: SPIN 2025.
Abstract
The semantics of alternating-time temporal logic (ATL) and the more expressive alternating-time -calculus (AMC) is standardly given in terms of concurrent game frames (CGF). The information required to interpret AMC formulas is equivalently represented in terms of effectivity frames in the sense of Pauly; in many cases, this representation is more compact than the corresponding CGF, and in principle allows for faster evaluation of coalitional modalities. In the present work, we investigate whether implementing a model checker based on effectivity frames leads to better performance in practice. We implement the translation from concurrent game frames to effectivity frames and analyse performance gains in model checking based on corresponding instantiations of a generic model checker for coalgebraic -calculi, using dedicated benchmark series as well as random systems and formulas. In the process, we also compare performance to the state-of-the-art ATL model checker MCMAS. Our results indicate that on large systems, the overhead involved in converting a CGF to an effectivity frame is often outweighed by the benefits in subsequent model checking.
| Item Type: | Conference Item (Unspecified) |
|---|---|
| Uncontrolled Keywords: | 4613 Theory Of Computation, 46 Information and Computing Sciences |
| Divisions: | Faculty of Science & Engineering Faculty of Science & Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 01 Jul 2025 08:15 |
| Last Modified: | 14 Jan 2026 00:53 |
| DOI: | 10.1007/978-3-032-06847-7_6 |
| Open Access URL: | https://arxiv.org/pdf/2506.01010 |
| Related Websites: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3193471 |
| Disclaimer: | The University of Liverpool is not responsible for content contained on other websites from links within repository metadata. Please contact us if you notice anything that appears incorrect or inappropriate. |
Altmetric
Altmetric