Towards partial order reductions for fragments of alternating-time temporal logic

Dembiński, P.; Jamroga, W.; Mazurkiewicz, A.; Penczek, W.

Artykuł - szczegóły

Tytuł artykułu

Towards partial order reductions for fragments of alternating-time temporal logic

Autorzy

Dembiński P. , Jamroga W. , Mazurkiewicz A. , Penczek W.

Treść / Zawartość

Pełne teksty:

Pobierz

Identyfikatory

Warianty tytułu

O redukcjach częścio-porządkowych dla fragmentów logiki temporalnej czasu alternatywnego

Języki publikacji

Abstrakty

A general semantics of strategic abilities of agents in asynchronous systems with and without perfect information is proposed, and some general complexity results for verification of strategic abilities in asynchronous systems are presented. A methodology for partial order reduction (POR) in verification of agents with imperfect information is developed, based on the notion of traces introduced by Mazurkiewicz. Two semantics of ATL∗ −X are considered and it is shown that for memoryless imperfect information (|=ir) contrary to memoryless perfect information (|=Ir), one can apply techniques known for LTL−X.

Raport definiuje ogólną semantykę dla strategicznych umiejętności agentów w systemach asynchronicznych z pełną i częściową informacją, oraz prezentuje ogólne wyniki dotyczące złożoności weryfikacji strategicznych możliwości w systemach asynchronicznych. Metoda redukcji częścio-porządkowych, wykorzystująca ślady Mazurkiewicza, została zastosowana do weryfikacji agentów z niepełną informacją. Dla rozważanych dwóch semantyk logiki ATL*_x zostało pokazane, że dla bezpamięciowej niepełnej informacji (|=ir) w przeciwieństwie do bezpamięciowej pełnej informacji (|=Ir), można zastosować metody znane dla LTL_x.

Słowa kluczowe

Alternating-Time Temporal Logic asynchronous systems partial order reduction traces

logika temporalna czasu alternującego systemy asynchroniczne redukcje częścio-porządkowe ślady

Wydawca

Instytut Podstaw Informatyki PAN

Czasopismo

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

Rocznik

2016

Tom

Nr 1036

Strony

1--32

Opis fizyczny

Bibliogr. 62 poz., rys.

Twórcy

autor

Dembiński P.

piotrd@ipipan.waw.pl

Instytut Podstaw Informatyki PAN ul. Jana Kazimierza 5 01-248 Warszawa, Polska

autor

Jamroga W.

jamroga@ipipan.waw.pl

Instytut Podstaw Informatyki PAN ul. Jana Kazimierza 5 01-248 Warszawa, Polska

autor

Mazurkiewicz A.

amaz@ipipan.waw.pl

Instytut Podstaw Informatyki PAN ul. Jana Kazimierza 5 01-248 Warszawa, Polska

autor

Penczek W.

penczek@ipipan.waw.pl

Instytut Podstaw Informatyki PAN ul. Jana Kazimierza 5 01-248 Warszawa, Polska

Bibliografia

[1] P. A. Abdulla, S. Aronis, B. Jonsson, and K. F. Sagonas. Optimal dynamic partial order reduction. In The 41st Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 373–384, 2014.
[2] R. Alur and T. A. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7–48, 1999.
[3] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS), pages 100–109. IEEE Computer Society Press, 1997.
[4] R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In Proceedings of CAV, volume 1427 of Lecture Notes in Computer Science, pages 521–525. Springer,1998.
[5] R. Alur, L. de Alfaro, R. Grossu, T. Henzinger, M. Kang, C. Kirsch, R. Majumdar, F. Mang, and B.-Y. Wang. jMocha: A model-checking tool that exploits design structure. In Proceedings of ICSE, pages 835–836. IEEE Computer Society Press, 2001.
[6] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672–713, 2002. doi: 10.1145/585265.585270.
[7] F. Belardinelli, R. Condurache, C. Dima, W. Jamroga, and A. Jones. Bisimulations for verification of strategic abilities with application to ThreeBallot voting protocol. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2017. IFAAMAS, 2017. To appear.
[8] N. Bulling and W. Jamroga. Alternating epistemic mu-calculus. In Proceedings of IJCAI-11, pages 109–114, 2011.
[9] N. Bulling and W. Jamroga. Comparing variants of strategic ability: How uncertainty and memory influence general properties of games. Journal of Autonomous Agents and Multi-Agent Systems, 28(3):474–518, 2014.
[10] N. Bulling, J. Dix, and W. Jamroga. Model checking logics of strategic ability: Complexity. In M. Dastani, K. Hindriks, and J.-J. Meyer, editors, Specification and Verification of Multi-Agent Systems, pages 125–159. Springer, 2010.
[11] S. Busard, C. Pecheur, H. Qu, and F. Raimondi. Improving the model checking of strategies under partial observability and fairness constraints. In Formal Methods and Software Engineering, volume 8829 of Lecture Notes in Computer Science, pages 27–42. Springer, 2014. ISBN 978-3-319-11736-2. doi: 10.1007/978-3-319-11737-9_3.
[12] S. Busard, C. Pecheur, H. Qu, and F. Raimondi. Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Information and Computation, 242:128–156, 2015. doi: 10.1016/j.ic.2015.03.014.
[13] K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya. Data-centric dynamic partial order reduction. CoRR, abs/1610.01188, 2016.
[14] T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. PRISMgames: A model checker for stochastic multi-player games. In Proceedings of TACAS, volume 7795 of Lecture Notes in Computer Science, pages 185–191. Springer, 2013.
[15] E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of Logics of Programs Workshop, volume 131 of Lecture Notes in Computer Science, pages 52–71, 1981.
[16] C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memoryefficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1(2/3):275–288, 1992.
[17] M. Dastani and W. Jamroga. Reasoning about strategies of multi-agent programs. In Proceedings of AAMAS2010, pages 625–632, 2010.
[18] C. Dima and F. Tiplea. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225, 2011.
[19] C. Dima, B. Maubert, and S. Pinchinat. The expressive power of epistemic µ-calculus. CoRR, abs/1407.5166, 2014.
[20] C. Dima, B. Maubert, and S. Pinchinat. Relating paths in transition systems: The fall of the modal mu-calculus. In Proceedings of MFCS, volume 9234 of Lecture Notes in Computer Science, pages 179–191.Springer, 2015. doi: 10.1007/978-3-662-48057-1_14.
[21] C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 110–121, 2005.
[22] R. Gerth, R. Kuiper, D. Peled, and W. Penczek. A partial order approach to branching time logic model checking. Information and Computation, 150:132–152, 1999.
[23] P. Godefroid. Using partial orders to improve automatic verification methods. In E. M. Clarke and R. P. Kurshan, editors, Proceedings of the 2nd International Conference on Computer Aided Verification (CAV’90), volume 3 of ACM/AMS DIMACS Series, pages 321–340, 1991.
[24] P. Godefroid and P. Wolper. A partial approach to model checking. Information and Computation, 110(2):305–326, 1994.
[25] U. Goltz, R. Kuiper, and W. Penczek. Propositional temporal logics and equivalences. In Proceedings of the 3rd International Conference on Concurrency Theory (CONCUR’92), volume 630 of LNCS, pages 222–236. Springer-Verlag, 1992.
[26] D. Guelev, C. Dima, and C. Enea. An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and modelchecking. Journal of Applied Non-Classical Logics, 21(1):93–131, 2011.
[27] W. Hoek and M. Wooldridge. Tractable multiagent planning for epistemic goals. In M. Gini, T. Ishida, C. Castelfranchi, and W. L. Johnson, editors, Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS’02), pages 1167–1174. ACM Press, 2002.
[28] X. Huang and R. van der Meyden. Symbolic model checking epistemic strategy logic. In Proceedings of AAAI, pages 1426–1432, 2014.
[29] G. Jakubowska and W. Penczek. Modelling and checking timed authentication of security protocols. Fundam. Inform., 79(3-4):363–378, 2007.
[30] G. Jakubowska and W. Penczek. Is your security protocol on time ? In Proceedings of International Symposium on Fundamentals of Software Engineering, International Symposium, FSEN, pages 65–80, 2007.
[31] G. Jakubowska, P. Dembinski, W. Penczek, and M. Szreter. Simulation ´of security protocols based on scenarios of attacks. Fundam. Inform., 93 (1-3):185–203, 2009.
[32] W. Jamroga. Some remarks on alternating temporal epistemic logic. In B. Dunin-Keplicz and R. Verbrugge, editors, Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003), pages 133–140, 2003.
[33] W. Jamroga and J. Dix. Model checking ATLir is indeed ∆P2-complete.In Proceedings of EUMAS’06, volume 223 of CEUR Workshop Proceedings. CEUR-WS.org, 2006.
[34] W. Jamroga and W. van der Hoek. Agents that know how to play. Fundamenta Informaticae, 63(2–3):185–219, 2004.
[35] W. Jamroga, M. Knapik, and D. Kurpiewski. Fixpoint approximation of strategic abilities under imperfect information. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2017. IFAAMAS, 2017. To appear.
[36] M. Kacprzak and W. Penczek. Unbounded model checking for alternating-time temporal logic. In Proceedings of AAMAS-04, pages 28 Prace IPI PAN • ICS PAS Reports 646–653. IEEE Computer Society, 2004. doi: 10.1109/AAMAS.2004. 10089.
[37] V. Kahlon, C. Wang, and A. Gupta. Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, pages 398–413, 2009.
[38] I. Kokkarinen, D. Peled, and A. Valmari. Relaxed visibility enhances partial order reductions. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV’97), volume 1254 of LNCS, pages 328–340. Springer-Verlag, 1997.
[39] I. Konnov, H. Veith, and J. Widder. SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pages 85–102, 2015.
[40] L. M. Kristensen and A. Valmari. Improved question-guided stubborn set methods for state properties. In Proceedings of the 21st International Conference on Applications and Theory of Petri Nets (ICATPN’00), volume 1825 of LNCS, pages 282–302. Springer-Verlag, 2000.
[41] O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312–360, 2000.
[42] M. Kurkowski and W. Penczek. Verifying security protocols modeled by networks of automata. Fundamenta Informaticae, 79(3-4):453–471, 2007.
[43] F. Laroussinie, N. Markey, and G. Oreiby. Model checking timed ATL for durational concurrent game structures. In FORMATS, volume 4202 of LNCS, pages 245–259. Springer, 2006.
[44] F. Laroussinie, N. Markey, and G. Oreiby. On the expressiveness and complexity of ATL. Logical Methods in Computer Science, 4:7, 2008.
[45] A. Lomuscio and F. Raimondi. MCMAS : A model checker for multiagent systems. In Proceedings of TACAS, volume 4314 of Lecture Notes in Computer Science, pages 450–454. Springer, 2006.
[46] A. Lomuscio and F. Raimondi. Model checking knowledge, strategies, and games in multi-agent systems. In Proceedings of AAMAS, pages 161–168, 2006. doi: 10.1145/1160633.1160660.
[47] A. Lomuscio, H. Qu, and F. Raimondi. MCMAS : A model checker for the verification multi-agent systems. In Proceedings of CAV, volume 5643 of Lecture Notes in Computer Science, pages 682–688. Springer, 2009.
[48] A. Lomuscio, W. Penczek, and H. Qu. Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. In 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), Toronto, Canada, May 10-14, 2010, Volume 1-3, pages 659–666, 2010.
[49] A. Lomuscio, W. Penczek, and H. Qu. Partial order reductions for model checking temporal-epistemic logics over interleaved multi-agent systems. Fundam. Inform., 101(1-2):71–90, 2010.
[50] A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: An open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer, 2015. doi: 10.1007/s10009-015-0378-x. Availabe online.
[51] A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Report Series, 6(78), 1977.
[52] A. Mazurkiewicz. Trace theory. In Advances in Petri Nets 1986, volume 255 of LNCS, pages 279–324. Springer-Verlag, 1986.
[53] A. Mazurkiewicz. Basic notions of trace theory. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS, pages 285–363. Springer-Verlag, 1988.
[54] D. Peled. All from one, one for all: On model checking using representatives. In Proceedings of the 5th International Conference on Computer Aided Verification, LNCS 697, pages 409–423. Springer-Verlag, 1993.
[55] D. Peled. Combining partial order reductions with on-the-fly modelchecking. In Proceedings of the 6th International Conference on Computer Aided Verification, LNCS 818, pages 377–390. Springer-Verlag, 1994.
[56] D. Peled. Partial order reductions: Model checking using representatives. In Proceedings of the 21st International Symposium on Mathematical Foundations of Computer Science (MFCS’96), volume 1113 of LNCS, pages 93–112. Springer-Verlag, 1996.
[57] D. Peled. Ten years of partial-order reductions. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV’98), volume 1427 of LNCS, pages 17–28. Springer-Verlag, 1998.
[58] W. Penczek, M. Szreter, R. Gerth, and R. Kuiper. Improving partial order reductions for universal branching time properties. Fundamenta Informaticae, 43:245–267, 2000.
[59] J. Pilecki, M. Bednarczyk, and W. Jamroga. Synthesis and verification of uniform strategies for multi-agent systems. In Proceedings of CLIMA XV, volume 8624 of Lecture Notes in Computer Science, pages 166–182. Springer, 2014.
[60] F. Raimondi. Model Checking Multi-Agent Systems. PhD thesis, University College London, 2006.
[61] P. Schnoebelen. The complexity of temporal model checking. In Advances in Modal Logics, Proceedings of AiML 2002. World Scientific, 2003.
[62] P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2):82–93, 20

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).

Typ dokumentu

Bibliografia

Identyfikator YADDA

bwmeta1.element.baztech-94b1edc5-6b4c-4d96-af6c-8c56294ec5c2