Abstract
In a former work, we have presented/implemented a framework for modeling and verifying multi-agent systems, using hybrid automata. To specify properties of those systems, one needs a specification language that brings, at the same level of specification, both the qualitative and quantitative requirements. For this aim, there have been proposed several temporal logics with either event or state based approach. Both approaches have their pros and cons which should not be played off against each other. This paper contributes to present a variant of temporal logics which combines the expressiveness of both approaches. Using this proposed logic, we are able reason about many properties in a concise and intuitive manner. In particular, we concentrate on those types of properties that can be verified using reachability analysis. Hence these properties can be verified directly within our implemented framework.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)
Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.: Logics and Models of Real Time: A Survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)
Alur, R., Henzinger, T.: A really temporal logic. Journal of the ACM (JACM) 41(1), 203 (1994)
Alur, R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering 22(3), 181–201 (1996)
Ammar, A.M.: Hybrid Multi-agent Systems: Modeling, Specification and Verification. Doctoral dessertation, Department of Computer Science, University of Koblenz-landau (2010)
Bacchus, F., Kabanza, F.: Using temporal logics to express search control knowledge for planning. Artificial Intelligence 116(1-2), 123–191 (2000)
Bellini, P., Mattolini, R., Nesi, P.: Temporal logics for real-time system specification. ACM Comput. Surv. 32(1), 12–42 (2000)
Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20(3), 207–226 (1983)
Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Uppaal—a tool suite for automatic verification of real-time systems. In: Proceedings of the DIMACS/SYCON Workshop on Hybrid Systems III: Verification and Control, pp. 232–243. Springer-Verlag New York, Inc., Secaucus (1996)
Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Formal Aspects of Computing 17, 461–483 (2005), 10.1007/s00165-005-0071-z
Egerstedt, M.: Behavior Based Robotics Using Hybrid Automata. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 103–116. Springer, Heidelberg (2000)
El Fallah-Seghrouchni, A., Degirmenciyan-Cartault, I., Marc, F.: Framework for Multi-agent Planning Based on Hybrid Automata. In: Mařík, V., Müller, J.P., Pěchouček, M. (eds.) CEEMAS 2003. LNCS (LNAI), vol. 2691, pp. 226–235. Springer, Heidelberg (2003)
Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. Real-Time Syst. 4(4), 331–352 (1992)
Furbach, U., Murray, J., Schmidsberger, F., Stolzenburg, F.: Hybrid Multiagent Systems with Timed Synchronization – Specification and Model Checking. In: Dastani, M., El Fallah Seghrouchni, A., Ricci, A., Winikoff, M. (eds.) ProMAS 2007. LNCS (LNAI), vol. 4908, pp. 205–220. Springer, Heidelberg (2008)
Giunchiglia, F., Traverso, P.: Planning as Model Checking. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 1–20. Springer, Heidelberg (2000)
Harel, E., Lichtenstein, O., Pnueli, A.: Explicit clock temporal logic. In: Proceedings of Fifth Annual IEEE Symposium on Logic in Computer Science, Philadelphia, Pennsylvania, USA, June 4-7, pp. 402–413. IEEE Computer Society (1990)
Henzinger, T.: The theory of hybrid automata. In: Proceedings of the 11th Annual Symposium on Logic in Computer Science, New Brunswick, NJ, pp. 278–292. IEEE Computer Society Press (1996)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: A User Guide to HyTech. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 41–71. Springer, Heidelberg (1995)
Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What’s Decidable about Hybrid Automata? Journal of Computer and System Sciences 57(1), 94–124 (1998)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Hytech: A Model Checker for Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460–463. Springer, Heidelberg (1997)
Hindriks, K.V., van der Hoek, W., van Riemsdijk, M.B.: Agent programming with temporally extended goals. In: Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2009, Richland, SC, vol. 1, pp. 137–144. International Foundation for Autonomous Agents and Multiagent Systems (2009)
Hutzler, G., Klaudel, H., Wang, D.Y.: Towards Timed Automata and Multi-agent Systems. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A. (eds.) FAABS 2004. LNCS (LNAI), vol. 3228, pp. 161–172. Springer, Heidelberg (2004)
Kindler, E., Vesper, T.: ESTL: A Temporal Logic for Events and States. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol. 1420, pp. 365–384. Springer, Heidelberg (1998)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)
Mohammed, A., Furbach, U.: Modeling multi-agent logistic process system using hybrid automata. In: Ultes-Nitsche, U., Moldt, D., Augusto, J.C. (eds.) Proceedings of the 7th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2008, Barcelona, Spain, pp. 141–149. INSTICC Press (2008); Held in conjunction with 10th International Conference on Enterprise Information Systems (ICEIS 2008)
Mohammed, A., Furbach, U.: Multi-Agent Systems: Modeling and Verification Using Hybrid Automata. In: Braubach, L., Briot, J.-P., Thangarajah, J. (eds.) ProMAS 2009. LNCS (LNAI), vol. 5919, pp. 49–66. Springer, Heidelberg (2010)
Nau, D., Ghallab, M., Traverso, P.: Automated Planning: Theory & Practice. Morgan Kaufmann Publishers Inc., San Francisco (2004)
Ostroff, J., Wonham, W.: A framework for real-time discrete event control. IEEE Transactions on Automatic Control 35(4), 386–397 (1990)
Platzer, A.: Differential Logic for Reasoning About Hybrid Systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 746–749. Springer, Heidelberg (2007)
Platzer, A.: A Temporal Dynamic Logic for Verifying Hybrid System Invariants. In: Artemov, S., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 457–471. Springer, Heidelberg (2007)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science 1977, pp. 46–57 (1977)
Pnueli, A., Harel, E.: Applications of Temporal Logic to the Specification of Real-Time Systems. In: Joseph, M. (ed.) FTRTFT 1988. LNCS, vol. 331, pp. 84–98. Springer, Heidelberg (1988)
Schwarz, C., Mohammed, A., Stolzenburg, F.: A tool environment for specifying and verifying multi-agent systems. In: Filipe, J., Fred, A., Sharp, B. (eds.) Proceedings of the 2nd International Conference on Agents and Artificial Intelligence, vol. 2, pp. 323–326. INSTICC Press (2010)
Van Benthem, J., ter Meulen, A. (eds.): Handbook of Logic and language. Elsevier (1997)
Yovine, S.: Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer (STTT) 1(1), 123–133 (1997)
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
Mohammed, A., Furbach, U. (2012). MAS: Qualitative and Quantitative Reasoning. In: Dennis, L., Boissier, O., Bordini, R.H. (eds) Programming Multi-Agent Systems. ProMAS 2011. Lecture Notes in Computer Science(), vol 7217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31915-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-31915-0_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31914-3
Online ISBN: 978-3-642-31915-0
eBook Packages: Computer ScienceComputer Science (R0)