Abstract
Constraint automata have been introduced to provide a compositional, operational semantics for the exogenous coordination language Reo, but they can also serve interface specification for components and an operational model for other coordination languages. Constraint automata have been used as basis for equivalence checking and model checking temporal logical properties. The main contribution of this paper is to reason about the local view and interaction and cooperation facilities of individual components or coalitions of components by means of a multi-player semantics for constraint automata. We introduce a temporal logic framework that combines classical features of alternating-time logic (\({\it ATL}\)) for concurrent games with special operators to specify the observable data flow at the I/O-ports of components. Since constraint automata support any kind of synchronous and asynchronous peer-to-peer communication, the resulting game structure is non-standard and requires a series of nontrivial adaptations of the \({\it ATL}\) model checking algorithm.
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
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49, 672–713 (2002)
Arbab, F.: Reo: A channel-based coordination model for component composition. Mathematical Structures in Computer Science 14(3), 329–366 (2004)
Arbab, F., Baier, C., de Boer, F., Rutten, J.J.M.M.: Models and temporal logics for timed component connectors. In: Proc. of SEFM, pp. 198–207. IEEE CS Press, Los Alamitos (2004)
Arbab, F., Baier, C., de Boer, F., Rutten, J.J.M.M., Sirjani, M.: Synthesis of Reo circuits for implementation of component connector automata specifications. In: Jacquet, J.-M., Picco, G.P. (eds.) COORDINATION 2005. LNCS, vol. 3454, Springer, Heidelberg (2005)
Azhar, S., Peterson, G.L., Reif, J.H.: On multiplayer non-cooperative games of incomplete information: Part 1&2. Technical report, Durham, NC, USA (1991)
Baier, C., Sirjani, M., Arbab, F., Rutten, J.J.M.M.: Modeling component connectors in Reo by constraint automata. In: Science of Computer Programming 61, pp. 75–113 (2006)
Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.F.: Algorithms for omega-regular games with imperfect information. CoRR, abs/0706.2619 (2007)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS 8(2), 244–263 (1986)
de Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: Proc. of LICS, pp. 141–154 (January 2000)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: FSE Proc., pp. 109–120. ACM Press, New York (2001)
de Wulf, M., Doyen, L., Raskin, J.-F.: A lattice theory for solving games of imperfect information. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 153–168. Springer, Heidelberg (2006)
Fischer, M.J., Ladner, R.J.: Propositional dynamic logic of regular programs. Journal of Computer and System Science 8, 194–211 (1979)
Fitoussi, D., Tennenholtz, M.: Choosing social laws for multi-agent systems: minimality and simplicity. Artif. Intell. 119(1-2), 61–101 (2000)
Francez, N.: Fairness. Springer, Heidelberg (1986)
Grosu, R., Rumpe, B.: Concurrent timed port automata. Technical Report TUM-I9533, Techn. Univ. München (1995), http://www4.informatik.tu-muenchen.de/reports/
Hoek, W.v.d., Roberts, M., Wooldridge, M.: Knowledge and social laws. In: AAMAS, pp. 674–681 (2005)
Hoek, W.v.d., Wooldridge, M.: Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica 75(1), 125–157 (2003)
Klüppelholz, S., Baier, C.: Symbolic model checking for channel-based component connectors. In: Proc. of FOCLASA 2006. ENTCS, vol. 175(2), pp. 19–37 (2007)
Klüppelholz, S., Baier, C.: Alternating-Time Stream Logic for Multi-Agent Systems. Technical report, Technical University Dresden (2008), http://wwwtcs.inf.tu-dresden.de/~klueppel/ASLKB2008.pdf
Lynch, N., Tuttle, M.R.: An introduction to input/output automata. CWI Quarterly 2(3), 219–246 (1989)
Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274–301 (1984)
Schobbens, P.Y.: Alternating-time logic with imperfect recall. In: Proc. of LCMAS. ENTCS, vol. 85(2), pp. 1–12 (2004)
Wolper, P.: Specification and synthesis of communicating processes using an extended temporal logic. In: Proc. of POPL, pp. 20–33 (1982)
Wooldridge, M.: Social laws in alternating time. In: Lomuscio, A., Nute, D. (eds.) DEON 2004. LNCS (LNAI), vol. 3065, p. 2. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klüppelholz, S., Baier, C. (2008). Alternating-Time Stream Logic for Multi-agent Systems. In: Lea, D., Zavattaro, G. (eds) Coordination Models and Languages. COORDINATION 2008. Lecture Notes in Computer Science, vol 5052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68265-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-68265-3_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68264-6
Online ISBN: 978-3-540-68265-3
eBook Packages: Computer ScienceComputer Science (R0)