Abstract
We present a SAT-based bounded model checking (BMC) method for the weighted interpreted systems (i.e. interpreted systems augmented to include a weight function, one per each agent, that associates weights with actions, which are arbitrary natural numbers) and for properties expressible in the existential fragment of a weighted linear temporal logic with epistemic components (WELTLK). Since in BMC we translate both the system model and the checked specification to a propositional formula that is later analysed by a SAT-solver, we report on a propositional encoding of both the weighted interpreted systems and the WELTLK formulae. This encoding is designed specifically for managing weighted temporal operators and knowledge operators, which are commonly found in properties of multi-agent systems in models of which we assume that acting of agents may cost. We implemented the proposed BMC algorithm as a new module of VerICS, and we evaluated it by means of the following two examples: a weighted generic pipeline paradigm and a weighted bits transmission problem.
Partly supported by National Science Center under the grant No. 2011/01/B/ST6/05317.
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
Lomuscio, A., Sergot, M.: Violation, error recovery, and enforcement in the bit transmission problem. Imperial College Press (2002)
Biere, A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 4, 75–97 (2008)
Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, ch. 16, pp. 996–1071. Elsevier Science Publishers (1990)
Fabre, E., Jezequel, L.: Distributed optimal planning: an approach by weighted automata calculus. In: Proceedings of CDC 2009, pp. 211–216. IEEE (2009)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press (1995)
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)
Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae 85(1-4), 313–328 (2008)
Levesque, H.: A logic of implicit and explicit belief. In: Proceedings of the 6th National Conference of the AAAI, pp. 198–202. Morgan Kaufman (1984)
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)
Lomuscio, A., Sergot, M.: Deontic interpreted systems. Studia Logica 75(1), 63–92 (2003)
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)
Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2003)
Penczek, W., Woźna-Szcześniak, B., Zbrzezny, A.: Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems. Fundamenta Informaticae 119(3-4), 373–392 (2012)
Wooldridge, M.: An introduction to multi-agent systems. John Wiley (2002)
Woźna-Szcześniak, B.: SAT-based bounded model checking for weighted deontic interpreted systems. In: Correia, L., Reis, L.P., Cascalho, J. (eds.) EPIA 2013. LNCS, vol. 8154, pp. 444–455. Springer, Heidelberg (2013)
Zbrzezny, A.: A new translation from ECTL* to SAT. Fundamenta Informaticae 120(3-4), 377–397 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Woźna-Szcześniak, B., Zbrzezny, A.M., Zbrzezny, A. (2013). SAT-Based Bounded Model Checking for Weighted Interpreted Systems and Weighted Linear Temporal Logic. In: Boella, G., Elkind, E., Savarimuthu, B.T.R., Dignum, F., Purvis, M.K. (eds) PRIMA 2013: Principles and Practice of Multi-Agent Systems. PRIMA 2013. Lecture Notes in Computer Science(), vol 8291. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-44927-7_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-44927-7_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-44926-0
Online ISBN: 978-3-642-44927-7
eBook Packages: Computer ScienceComputer Science (R0)