Cheap CTL Compassion in NuSMV

Hausmann D, Litak TM, Rauch C, Zinner M (2020)

Publication Type: Conference contribution

Publication year: 2020

Journal

Lecture Notes in Computer Science Springer Verlag

Publisher: Springer

Book Volume: 11990 LNCS

Pages Range: 248-269

Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Event location: New Orleans, LA US

ISBN: 9783030393212

DOI: 10.1007/978-3-030-39322-9_12

Abstract

We discuss expansions of with connectives able to express Streett fairness objectives for single paths. We focus on: (Extended) Streett-Fair inspired by a seminal paper of Emerson and Lei. Unlike several other fair extensions of, our entire formalism (not just a subclass of formulas in some canonical form) allows a succinct embedding into the-calculus, while being able to express concisely all relevant types of path-based fairness objectives. We implement our syntax in the well-known symbolic model checker NuSMV, consequently also implementing model checking with “compassion” objectives. Since the-calculus embedding requires only alternation depth two, the resulting specifications correspond to parity games with two priorities. This allows a comparison of the performance of our NuSM with existing parity game solvers (both explicit and symbolic). The advantages of the symbolic approach seem to extend to fair model checking.

Authors with CRIS profile

Daniel Hausmann Lehrstuhl für Informatik 8 (Theoretische Informatik) Tadeusz Michal Litak Lehrstuhl für Informatik 8 (Theoretische Informatik) Christoph Rauch Lehrstuhl für Informatik 8 (Theoretische Informatik)

How to cite

APA:

Hausmann, D., Litak, T.M., Rauch, C., & Zinner, M. (2020). Cheap CTL Compassion in NuSMV. In Dirk Beyer, Damien Zufferey (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 248-269). New Orleans, LA, US: Springer.

MLA:

Hausmann, Daniel, et al. "Cheap CTL Compassion in NuSMV." Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2020, New Orleans, LA Ed. Dirk Beyer, Damien Zufferey, Springer, 2020. 248-269.

BibTeX: Download