Abstract
An implementation of a recent algorithm (Vüge, Jurdzinski, to appear in CAV 2000) for the construction of winning strategies in infinite games is presented. The games under consideration are “finite-state parity games”, i.e. games over finite graphs where the winning condition is inherited from ω-automata with parity acceptance. The emphasis of the paper is the development of a user interface which supports the researcher in case studies for algorithms of ω-automata theory. Examples of such case studies are provided which might help in evaluating the (so far open) asymptotic runtime of the presented algorithm.
Both authors are supported by the Deutsche Forschungsgemeinschaft (DFG), project Th 352/5-3.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
N. Buhrke, H. Lescow, and J. Vöge. Strategy construction in infinite games with Streett and Rabin chain winning conditions. In T. Magaria and B. Steffen, editors, TACAS’96, volume 1055 of LNCS, pages 207–225. Springer, 1996.
E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus and determinacy. In Proc. 32nd IEEE Symp. on the Foundations of Computing, pages 368–377, 1991.
E.A. Emerson, C.S. Jutla, and A.P. Sistla. On model checking for fragments of μ-calculus. In C. Courcoubetis, editor, Computer Aided Verification, number 697 in Lecture Notes in Computer Science, pages 385–396, Berlin, 1993. Springer Verlag.
M. Jurdziński. Small progress measures for solving parity games. In H. Reichel and S. Tison, editors, STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings, volume 1770 of LNCS, pages 290–301, Lille, France, February 2000. Springer.
R. McNaughton. Infinite games played on finite graphs. Ann. Pure Appl Logic, 65:149–184, 1993.
A. Puri. Theory of hybrid systems and discrete event systems. Ph.d. thesis, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720, Dec. 1995. Memorandum No. UCB/ERL M95/113.
W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Language Theory, volume III, pages 389–455. Springer-Verlag, New York, 1997.
J. Vöge and M. Jurdziński. A discrete strategy improvement algorithm for solving parity games. In E.A. Emerson and A.P. Sistla, editors, Computer Aided Verification (CAV), LNCS. Springer Verlag, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmitz, D., Vöge, J. (2001). Implementation of a Strategy Improvement Algorithm for Finite-State Parity Games. In: Yu, S., Păun, A. (eds) Implementation and Application of Automata. CIAA 2000. Lecture Notes in Computer Science, vol 2088. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44674-5_22
Download citation
DOI: https://doi.org/10.1007/3-540-44674-5_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42491-8
Online ISBN: 978-3-540-44674-3
eBook Packages: Springer Book Archive