Abstract
In probabilistic game structures, probabilistic alternating simulation (PA-simulation) relations preserve formulas defined in probabilistic alternating-time temporal logic with respect to the behaviour of a subset of players. We propose a partition based algorithm for computing the largest PA-simulation. It is to our knowledge the first such algorithm that works in polynomial time. Our solution extends the generalised coarsest partition problem (GCPP) to a game-based setting with mixed strategies. The algorithm has higher complexities than those in the literature for non-probabilistic simulation and probabilistic simulation without mixed actions, but slightly improves the existing result for computing probabilistic simulation with respect to mixed actions.
This is a preview of subscription content, log in via an institution to check access.
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
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of ACM 49(5), 672–713 (2002)
Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating Refinement Relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. Journal of Computer and System Sciences 60(1), 187–231 (2000)
Bustan, D., Grumberg, O.: Simulation based minimization. ACM Transactions on Computational Logic 4(2), 181–206 (2003)
Cattani, S., Segala, R.: Decision Algorithms for Probabilistic Bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–386. Springer, Heidelberg (2002)
Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The complexity of quantitative concurrent parity games. In: Proc. SODA, pp. 678–687. ACM (2006)
Chatterjee, K., de Alfaro, L., Majumdar, R., Raman, V.: Algorithms for game metrics (full version). Logical Methods in Computer Science 6(3:13), 1–27 (2010)
Clarke, E.M., Emerson, E.A.: Synthesis of Synchronization Skeletons for Branching-Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
de Alfaro, L.: Quantitative Verification and Control Via the Mu-Calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 103–127. Springer, Heidelberg (2003)
de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. In: Proc. FOCS, pp. 564–575. IEEE CS (1998)
de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. Journal of Computer and System Sciences 68(2), 374–397 (2004)
de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game refinement relations and metrics. Logic Methods in Computer Science 4(3:7), 1–28 (2008)
Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: Coarsest partition problems. Journal of Automatic Reasoning 31(1), 73–103 (2003)
Grumberg, O., Long, D.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)
Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. FOCS, pp. 453–462. IEEE CS (1995)
Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proc. LICS, pp. 266–277. IEEE CS (1991)
Karmakar, N.: A new polynomial-time algorithm for linear programming. Combinatorica 4(4), 373–395 (1984)
Ranzato, F., Tapparo, F.: A new efficient simulation equivalence algorithm. In: Proc. LICS, pp. 171–180. IEEE CS (2007)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2(2), 250–273 (1995)
Shapley, L.S.: Stochastic games. Proc. National Academy of Science 39, 1095–1100 (1953)
Tan, L., Cleaveland, R.: Simulation Revisited. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 480–495. Springer, Heidelberg (2001)
van Glabbeek, R.J., Ploeger, B.: Correcting a Space-Efficient Simulation Algorithm. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 517–529. Springer, Heidelberg (2008)
von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior. Princeton University Press (1947)
Zhang, C., Pang, J.: On Probabilistic Alternating Simulations. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIP AICT, vol. 323, pp. 71–85. Springer, Heidelberg (2010)
Zhang, L.: A Space-Efficient Probabilistic Simulation Algorithm. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 248–263. Springer, Heidelberg (2008)
Zhang, L., Hermanns, H., Eisenbrand, F., Jansen, D.N.: Flow faster: Efficient decision algorithms for probabilistic simulations. Logical Methods in Computer Science 4(4:6), 1–43 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, C., Pang, J. (2012). An Algorithm for Probabilistic Alternating Simulation. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds) SOFSEM 2012: Theory and Practice of Computer Science. SOFSEM 2012. Lecture Notes in Computer Science, vol 7147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27660-6_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-27660-6_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27659-0
Online ISBN: 978-3-642-27660-6
eBook Packages: Computer ScienceComputer Science (R0)