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 \(\textsc{vctl}^\star\) – an extension of \(\textsc{ctl}^\star\) by variables, which is capable of specifying properties of abstract systems. We show that \(\textsc{vctl}^\star\) logically characterizes the simulation pre-order between abstract systems. That is, that satisfaction of \(\textsc{vactl}^\star\), namely the universal fragment of \(\textsc{vctl}^\star\), is preserved in simulating abstract systems. For the second direction, we show that if an abstract system \({\cal{A}}_2\) does not simulate an abstract system \({\cal{A}}_1\), then there exists a \(\textsc{vactl}\) formula that distinguishes \({\cal{A}}_1\) from \({\cal{A}}_2\). Finally, we present a game-theoretic approach to simulation of abstract systems and show that the prover wins the game iff \({\cal{A}}_2\) simulates \({\cal{A}}_1\). Further, if \({\cal{A}}_2\) does not simulate \({\cal{A}}_1\), then the refuter wins the game and his winning strategy corresponds to a \(\textsc{vactl}\) formula that distinguishes \({\cal{A}}_1\) from \({\cal{A}}_2\). Thus, the many appealing practical advantages of simulation are lifted to the setting of data-parameterized abstract systems.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Paige, R., Bloom, B.: Transformational design and implementation of a new efficient solution to the ready simulation problem. Science of Computer Programming 24, 189–220 (1996)
Bensalem, S., Bouajjani, A., Loiseaux, C., Sifakis, J.: Property preserving simulations. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 260–273. Springer, Heidelberg (1993)
Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data trees and XML reasoning. J. ACM 56(3), 1–48 (2009)
Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: LICS 2006, pp. 7–16 (2006)
Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science 59, 115–131 (1988)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: A semantics-based tool for the verification of concurrent systems. ACM TOPLAS 15, 36–72 (1993)
Damm, W., Pnueli, A.: Verifying out-of-order executions. In: Proc. 9th Conf. on Correct Hardware Design and Verification Methods, pp. 23–47. Chapman & Hall (1997)
Demri, S., D’Souza, D.: An automata-theoretic approach to constraint LTL. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 121–132. Springer, Heidelberg (2002)
German, S., Prasad Sistla, A.: Reasoning about systems with many processes. Journal of the ACM 39, 675–735 (1992)
Grumberg, O., Kupferman, O., Sheinvald, S.: Variable automata over infinite alphabets. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 561–572. Springer, Heidelberg (2010)
Grumberg, O., Kupferman, O., Sheinvald, S.: Model checking systems and specifications with parameterized atomic propositions. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 122–136. Springer, Heidelberg (2012)
Grumberg, O., Kupferman, O., Sheinvald, S.: An automata-theoretic approach to reasoning about parameterized systems and specifications. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 397–411. Springer, Heidelberg (2013)
Grumberg, O., Long, D.E.: Model checking and modular verification. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 250–265. Springer, Heidelberg (1991)
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languagues and Systems 16(3), 843–871 (1994)
Hallé, S., Villemaire, R., Cherkaoui, O.: Ctl model checking for labelled tree queries. In: TIME, pp. 27–35 (2006)
Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. Information and Computation 173(1), 64–81 (2002)
Kaminski, M., Zeitlin, D.: Extending finite-memory automata with non-deterministic reassignment. In: Csuhaj-Varjú, Ézik, Z.E. (eds.) AFL, pp. 195–207 (2008)
Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 381–393. Springer, Heidelberg (2003)
Lamport, L.: Specifying concurrent program modules. ACM Transactions on Programming Languagues and Systems 5, 190–222 (1983)
Lazić, R.S.: Safely freezing LTL. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 381–392. Springer, Heidelberg (2006)
Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proc. 6th ACM Symp. on Principles of Distributed Computing, pp. 137–151 (1987)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)
Milner, R.: An algebraic definition of simulation between programs. In: Proc. 2nd Int. Joint Conf. on Artificial Intelligence, pp. 481–489. British Computer Society (1971)
Neven, F., Schwentick, T., Vianu, V.: Towards regular languages over infinite alphabets. In: Sgall, J., Pultr, A., Kolman, P. (eds.) MFCS 2001. LNCS, vol. 2136, pp. 560–572. Springer, Heidelberg (2001)
Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 510–584. Springer, Heidelberg (1986)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Shemesh, Y., Francez, N.: Finite-state unification automata and relational languages. Information and Computation 114, 192–213 (1994)
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: Proc. 5th ACM Symp. on Theory of Computing, pp. 1–9 (1973)
Tan, T.: Pebble Automata for Data Languages: Separation, Decidability, and Undecidability. PhD thesis, Technion - Computer Science Department (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Grumberg, O., Kupferman, O., Sheinvald, S. (2014). A Game-Theoretic Approach to Simulation of Data-Parameterized Systems. In: Cassez, F., Raskin, JF. (eds) Automated Technology for Verification and Analysis. ATVA 2014. Lecture Notes in Computer Science, vol 8837. Springer, Cham. https://doi.org/10.1007/978-3-319-11936-6_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-11936-6_25
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11935-9
Online ISBN: 978-3-319-11936-6
eBook Packages: Computer ScienceComputer Science (R0)