Paper Info
Title
A Game-Theoretic Approach to Simulation of Data-Parameterized Systems.
Abstract
This work focuses on data-parameterized abstract systems that extend standard modelling by allowing atomic propositions to be parameterized by variables that range over some infinite domain. These variables may range over process ids, message numbers, etc. Thus, abstract systems enable simple modelling of infinite-state systems whose source of infinity is the data. We define and study a simulation pre-order between abstract systems. The definition extends the definition of standard simulation by referring also to variable assignments. We define VCTL star - an extension of CTL star by variables, which is capable of specifying properties of abstract systems. We show that VCTL star logically characterizes the simulation pre-order between abstract systems. That is, that satisfaction of VACTL(star), namely the universal fragment of VCTL star, is preserved in simulating abstract systems. For the second direction, we show that if an abstract system A(2) does not simulate an abstract system A(1), then there exists a VACTL formula that distinguishes A(1) from A(2). Finally, we present a game-theoretic approach to simulation of abstract systems and show that the prover wins the game iff A(2) simulates A(1). Further, if A(2) does not simulate A(1), then the refuter wins the game and his winning strategy corresponds to a VACTL formula that distinguishes A(1) from A(2). Thus, the many appealing practical advantages of simulation are lifted to the setting of data-parameterized abstract systems.
Year
DOI
Venue
2014
10.1007/978-3-319-11936-6_25
Lecture Notes in Computer Science
Field
DocType
Volume
Discrete mathematics,Parameterized complexity,Computer science,Infinity,Game theoretic
Conference
8837
ISSN
Citations 
PageRank 
0302-9743
3
0.38
References 
Authors
24
3
Name
Order
Citations
PageRank
Orna Grumberg14361351.99
Orna Kupferman23548223.79
Sarai Sheinvald3585.19