Abstract
We propose a property-preserving refinement/abstraction theory for Kripke Modal Labelled Transition Systems incorporating not only state mapping but also label and proposition lumping, in order to have a compact but informative abstraction. We develop a 3-valued version of Public Announcement Logic (PAL) which has a dynamic operator that changes the model in the spirit of public broadcasting. We prove that the refinement relation on static models assures us to safely reason about any dynamic properties in terms of PAL-formulas on the abstraction of a model. The theory is in particular interesting and applicable for an epistemic setting as the example of the Muddy Children puzzle shows, especially in the view of the growing interest for epistemic modelling and (automatic) verification of communication protocols.
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
Baltag, A., Moss, L.S.: Logics for epistemic programs. Synthese 139(2), 165–224 (2004)
van Benthem, J., van Eijck, J., Kooi, B.: Logics of communication and change. Information and Computation (2006)
Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142. Springer, Heidelberg (2004)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. In: Practical Cryptography for Data Internetworks. IEEE Computer Society Press, Los Alamitos (1996)
Dechesne, F., Mousavi, M., Orzan, S.M.: Operational and epistemic approaches to protocol analysis: Bridging the gap. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790. Springer, Heidelberg (2007)
Dechesne, F., Wang, Y.: Dynamic epistemic verification of security protocols: framework and case study. In: A Meeting of the minds: Proceedings LORI workshop. Texts in Computer Science, pp. 129–144 (2007)
van Eijck, J.: DEMO program and documentation (2005), http://www.cwi.nl/~jve/demo/
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 137–150. Springer, Heidelberg (2002)
Halpern, J.Y., O’Neill, K.R.: Anonymity and information hiding in multiagent systems. Journal of Computer Security, 483–514 (2005)
van der Hoek, W., Wooldridge, M.: Model checking knowledge and time. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 95–111. Springer, Heidelberg (2002)
Hommersom, A., Meyer, J.-J., de Vink, E.P.: Update semantics of security protocols. Synthese 142, 229–267 (2004); Knowledge, Rationality and Action subseries
Hughes, D., Shmatikov, V.: Information hiding, anonymity and privacy: A modular approach. Journal of Computer Security 12(1), 3–36 (2004)
Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028. Springer, Heidelberg (2001)
Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, pp. 232–246 (1989)
Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings LICS, pp. 203–210 (1988)
van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: Proc. CSFW 2004, pp. 280–291. IEEE, Los Alamitos (2004)
Plaza, J.A.: Logics of public communications. In: Proceedings ISMIS 1989, pp. 201–216 (1989)
Raimondi, F., Lomuscio, A.: Automatic verification of deontic interpreted systems by model checking via OBDD’s. Journal of Applied Logic (2006)
van de Pol, J.C., Valero Espada, M.: Modal abstractions in μCRL*. In: AMAST, pp. 409–425 (2004)
van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamnic Epistemic Logic. Synthese Library, vol. 337. Springer, Heidelberg (2008)
van Eijck, J., Orzan, S.M.: Epistemic verification of anonymity. ENTCS, 168 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dechesne, F., Orzan, S., Wang, Y. (2008). Refinement of Kripke Models for Dynamics. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds) Theoretical Aspects of Computing - ICTAC 2008. ICTAC 2008. Lecture Notes in Computer Science, vol 5160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85762-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-85762-4_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85761-7
Online ISBN: 978-3-540-85762-4
eBook Packages: Computer ScienceComputer Science (R0)