×

zbMATH — the first resource for mathematics

Towards partial order reduction for model checking temporal epistemic logic. (English) Zbl 1226.68043
Peled, Doron A. (ed.) et al., Model checking and artificial intelligence. 5th international workshop, MoChArt 2008, Patras, Greece, July 21, 2008. Revised selected and invited papers. Berlin: Springer (ISBN 978-3-642-00430-8/pbk). Lecture Notes in Computer Science 5348. Lecture Notes in Artificial Intelligence, 106-121 (2009).
Summary: We introduce basic partial order reduction techniques in a temporal-epistemic setting. We analyse the semantics of interpreted systems with respect to the notions of trace-equivalence for the epistemic linear time logic LTLK\(_{ - X }\).
For the entire collection see [Zbl 1156.68006].
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B42 Logics of knowledge and belief (including belief change)
03B44 Temporal logic
68T27 Logic in artificial intelligence
68T42 Agent technology and artificial intelligence
Software:
MCK; MCMAS; Verics
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Dembinski, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B.z., Zbrzezny, A.: VerICS: A tool for verifying Timed Automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 278–283. Springer, Heidelberg (2003) · Zbl 1031.68546 · doi:10.1007/3-540-36577-X_20
[2] Diekert, V., Rozemberg, G. (eds.): The Book of Traces. World Scientific Publishing Co. Pte. Ltd., Singapore (1995)
[3] Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995) · Zbl 0839.68095
[4] Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004) · Zbl 1103.68614 · doi:10.1007/978-3-540-27813-9_41
[5] Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. Information and Computation 150, 132–152 (1999) · Zbl 1045.68588 · doi:10.1006/inco.1998.2778
[6] Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. ACM \(/\) AMS DIMACS Series, vol. 3, pp. 321–340 (1991) · Zbl 0786.68061 · doi:10.1007/BFb0023731
[7] Halpern, J., van der Meyden, R., Vardi, M.Y.: Complete axiomatisations for reasoning about knowledge and time. SIAM Journal on Computing 33(3), 674–703 (2003) · Zbl 1059.68127 · doi:10.1137/S0097539797320906
[8] Halpern, J., Moses, Y.: Knowledge and common knowledge in a distributed environment. Journal of the ACM 37(3), 549–587 (1984); A preliminary version appeared in Proc. 3rd ACM Symposium on Principles of Distributed Computing (1984) · Zbl 0699.68115 · doi:10.1145/79147.79161
[9] Holzmann, G., Peled, D.: Partial order reduction of the state space. In: First SPIN Workshop, Montréal, Quebec (1995)
[10] Kacprzak, M., Lomuscio, A., Penczek, W.: From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae 63(2,3), 221–240 (2004) · Zbl 1102.68107
[11] Kurbán, M.E., Niebert, P., Qu, H., Vogler, W.: Stronger reduction criteria for local first search. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 108–122. Springer, Heidelberg (2006) · Zbl 1168.68386 · doi:10.1007/11921240_8
[12] Lamport, L.: What good is temporal logic? In: IFIP Congress, pp. 657–668 (1983)
[13] Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006) · doi:10.1007/11691372_31
[14] Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems, vol. 1. Springer, Berlin (1992) · Zbl 0753.68003 · doi:10.1007/978-1-4612-0931-7
[15] McMillan, K.L.: A technique of a state space search based on unfolding. Formal Methods in System Design 6(1), 45–65 (1995) · Zbl 0829.68085 · doi:10.1007/BF01384314
[16] Parikh, R., Ramanujam, R.: Distributed processes and the logic of knowledge. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 256–268. Springer, Heidelberg (1985) · Zbl 0565.68025 · doi:10.1007/3-540-15648-8_21
[17] Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993) · doi:10.1007/3-540-56922-7_34
[18] Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2003) · Zbl 1111.68512
[19] Penczek, W., Szreter, M., Gerth, R., Kuiper, R.: Improving partial order reductions for universal branching time properties. Fundamenta Informaticae 43, 245–267 (2000) · Zbl 0966.68126
[20] Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic (2007) (to appear in Special issue on Logic-based agent verification) · Zbl 1122.68076
[21] Rosenschein, S.J.: Formal theories of ai in knowledge and robotics. New Generation Computing 3, 345–357 (1985) · Zbl 0596.68061 · doi:10.1007/BF03037076
[22] Valmari, A.: A stubborn attack on state explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991) · Zbl 0765.68147 · doi:10.1007/BFb0023729
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.