Abstract
This paper shows how multiagent systems can be modeled by a combination of UML statecharts and hybrid automata. This allows formal system specification on different levels of abstraction on the one hand and expressing real-time system behavior with continuous variables on the other hand. It is shown, how multi-robot systems can be modeled by hybrid and hierarchical state machines and how model checking techniques for hybrid automata can be applied. An enhanced synchronization concept is introduced that allows synchronization taking time and avoids state explosion to a certain extent.
This research is supported by the grants Fu 263/8 and Sto 421/2 from the German research foundation DFG within the special priority program 1125 on Cooperating Teams of Mobile Robots in Dynamic Environments.
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
Arai, T., Stolzenburg, F.: Multiagent systems specification by UML statecharts aiming at intelligent manufacturing. In: Proceedings of 1st International Joint Conference on Autonomous Agents & Multi-Agent Systems, pp. 11–18. ACM Press, New York (2002)
Bernstein, T., et al.: HAL – hybrid automaton language. Team project description (in German), Department of Automation and Computer Sciences, Hochschule Harz (2006)
Clocksin, W.F., Mellish, C.S.: Programming in Prolog, 4th edn. Springer, Berlin (1994)
Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)
Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology 5(4), 293–333 (1996)
Henzinger, T.: The theory of hybrid automata. In: Proceedings of the 11th Annual Symposium on Logic in Computer Science, pp. 278–292. IEEE Computer Society Press, Los Alamitos (1996)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: The Next Generation. In: IEEE Real-Time Systems Symposium, pp. 56–65 (1995)
Henzinger, T.A., Majumdar, R.: Symbolic model checking for rectangular hybrid systems. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 142–156 (2000)
Murray, J.: Specifying agent behaviors with UML statecharts and StatEdit. In: Polani, D., Browning, B., Bonarini, A., Yoshida, K. (eds.) RoboCup 2003. LNCS (LNAI), vol. 3020, Springer, Heidelberg (2004)
Murray, J., Stolzenburg, F.: Hybrid state machines with timed synchronization for multi-robot system specification. In: Bento, C., et al. (eds.) Proceedings of 12th Portuguese Conference on Artificial Intelligence, pp. 236–241. IEEE Inc, Los Alamitos (2005)
Murray, J., Stolzenburg, F., Arai, T.: Hybrid state machines with timed synchronization for multi-robot system specification. KI 3/06, 45–50 (2006)
Object Management Group, Inc. UML Specification, Version 1.5 (March 2003)
Object Management Group, Inc. UML 2.0 Superstructure Specification (October 2004)
Pnueli, A., Shalev, M.: What is in a step: On the semantics of statecharts. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 244–264. Springer, Heidelberg (1991)
Rao, A.S., Georgeff, M.P.: BDI-agents: from theory to practice. In: Proceedings of the First Intl. Conference on Multiagent Systems, San Francisco (1995)
Ruh, F.: A translator for cooperative strategies of mobile agents for four-legged robots. Master thesis, Dept. of Automation and Computer Sciences, Hochschule Harz (2007)
Stolzenburg, F.: Multiagent systems and RoboCup: Specification, analysis, and theoretical results. Habilitation, Universität Koblenz-Landau, Koblenz, Reviewers: Armin Cremers, Ulrich Furbach, and Klaus Troitzsch (2005)
Stolzenburg, F., Arai, T.: From the specification of multiagent systems by statecharts to their formal analysis by model checking: Towards safety-critical applications. In: Schillo, M., Klusch, M., Müller, J., Tianfield, H. (eds.) MATES 2003. LNCS (LNAI), vol. 2831, pp. 131–143. Springer, Heidelberg (2003)
Tadokoro, S., et al.: The RoboCup-Rescue project: A robotic approach to the disaster mitigation problem. In: Proceedings of IEEE International Conference on Robotics and Automation (ICRA 2000), pp. 4089–4104 (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Furbach, U., Murray, J., Schmidsberger, F., Stolzenburg, F. (2008). Hybrid Multiagent Systems with Timed Synchronization – Specification and Model Checking. In: Dastani, M., El Fallah Seghrouchni, A., Ricci, A., Winikoff, M. (eds) Programming Multi-Agent Systems. ProMAS 2007. Lecture Notes in Computer Science(), vol 4908. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79043-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-79043-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79042-6
Online ISBN: 978-3-540-79043-3
eBook Packages: Computer ScienceComputer Science (R0)