abstract={. In this paper we develop a new algorithm for deciding the winner in parity games, and hence also for the modal -calculus model checking. The design and analysis of the algorithm is based on a notion of game progress measures: they are witnesses for winning strategies in parity games. We characterize game progress measures as pre-fixed points of certain monotone operators on a complete lattice. As a result we get the existence of the least game progress measures and a straightforward way to compute them. The worst-case running time of our algorithm matches the best worst-case running time bounds known so far for the problem, achieved by the algorithms due to Browne et al., and Seidl. Our algorithm has better space complexity: it works in small polynomial space; the other two algorithms have exponential worst-case space complexity. 1 Introduction A parity game is an infinite path-forming game played by two players, player \# and player \#, on a graph with integer priorities assigned to...},
file={/home/qaristote/Zotero/storage/YFXEX8BA/Jurdzinski - 2000 - Small Progress Measures for Solving Parity Games.pdf;/home/qaristote/Zotero/storage/HEPKDQ2E/summary.html}
}
\ No newline at end of file
}
@article{stirlingBisimulationModalLogic1999,
title={Bisimulation, Modal Logic and Model Checking Games},
author={Stirling, C.},
year={1999},
month=jan,
volume={7},
pages={103--124},
publisher={{Oxford Academic}},
issn={1367-0751},
doi={10.1093/jigpal/7.1.103},
abstract={Abstract. We give a very brief introduction to how concurrent systems can be modelled within process calculi, as terms of an algebraic language whose behaviour},
file={/home/qaristote/Zotero/storage/93D4SGA7/Stirling - 1999 - Bisimulation, modal logic and model checking games.pdf;/home/qaristote/Zotero/storage/7M36QIW4/681726.html},
journal={Logic Journal of the IGPL},
language={en},
number={1}
}
@article{baldanAbstractionUptoTechniques2020,
title={Abstraction, {{Up}}-to {{Techniques}} and {{Games}} for {{Systems}} of {{Fixpoint Equations}}},
author={Baldan, Paolo and K{\"o}nig, Barbara and Padoan, Tommaso},
year={2020},
month=mar,
abstract={Systems of fixpoint equations over complete lattices, consisting of (mixed) least and greatest fixpoint equations, allow one to express a number of verification tasks such as model-checking of various kinds of specification logics or the check of coinductive behavioural equivalences. In this paper we develop a theory of approximation for systems of fixpoint equations in the style of abstract interpretation: a system over some concrete domain is abstracted to a system in a suitable abstract domain, with conditions ensuring that the abstract solution represents a sound/complete overapproximation of the concrete solution. Interestingly, up-to techniques, a classical approach used in coinductive settings to obtain easier or feasible proofs, can be interpreted as abstractions in a way that they naturally fit in our framework and extend to systems of equations. Additionally, relying on the approximation theory, we can provide a characterisation of the solution of systems of fixpoint equations over complete lattices in terms of a suitable parity game, generalising some recent work that was restricted to continuous lattices. The game view opens the way to the development of on-the-fly algorithms for characterising the solution of such equation systems.},
archivePrefix={arXiv},
eprint={2003.08877},
eprinttype={arxiv},
file={/home/qaristote/Zotero/storage/97A6VQ5S/Baldan et al. - 2020 - Abstraction, Up-to Techniques and Games for System.pdf;/home/qaristote/Zotero/storage/YX5NYYWR/2003.html},
journal={arXiv:2003.08877 [cs]},
keywords={Computer Science - Logic in Computer Science},
