Improving Parity Game Solvers with Justifications
Autor: | Maurice Bruynooghe, Marc Denecker, Ruben Lapauw |
---|---|
Přispěvatelé: | Beyer, Dirk, Zufferey, Damien |
Rok vydání: | 2020 |
Předmět: |
Model checking
Computer Science::Computer Science and Game Theory 050101 languages & linguistics Theoretical computer science Computer science 05 social sciences ComputingMilieux_PERSONALCOMPUTING 02 engineering and technology Directed graph Graph Automaton TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Parity game Computer Science::Logic in Computer Science Bounded function 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Parity (mathematics) Formal verification |
Zdroj: | Lecture Notes in Computer Science ISBN: 9783030393212 VMCAI |
DOI: | 10.1007/978-3-030-39322-9_21 |
Popis: | Parity games are infinite two-player games played on node-weighted directed graphs. Formal verification problems such as verifying and synthesizing automata, bounded model checking of LTL, CTL*, propositional µ-calculus, ...reduce to problems over parity games. The core problem of parity game solving is deciding the winner of some (or all) nodes in a parity game. In this paper, we improve several parity game solvers by using a justification graph. Experimental evaluation shows our algorithms improve upon the state-of-the-art. ispartof: pages:449-470 ispartof: Proceedings of VMCAI 2020 vol:11990 pages:449-470 ispartof: 21st International Conference on Verification, Model Checking, and Abstract Interpretation location:New Orleans date:19 Jan - 21 Jan 2020 status: Published online |
Databáze: | OpenAIRE |
Externí odkaz: |