×

Alternating-time stream logic for multi-agent systems. (English) Zbl 1192.68697

Summary: Constraint automata have been introduced to provide a uniform operational model for specifying service interfaces of components, the network that yields the glue code for the components, and the operational behavior of the composite system. Constraint automata have been used as the basis for equivalence checking and model checking temporal logical properties. This paper presents a multi-player semantics for constraint automata which serves to reason about controllability, interaction and cooperation facilities of individual components or coalitions of components in a given network. We introduce a temporal logic framework, called alternating-time stream logic, that combines classical features of alternating-time logic (ATL) for concurrent games with special operators for specifying regular conditions on the data streams in the network and on the write and read operations at the I/O-ports of the 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 to the semantics and verification algorithms for classical alternating-time approaches.

MSC:

68T42 Agent technology and artificial intelligence
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Reo
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alur, R.; Henzinger, T. A.; Kupferman, O.: Alternating-time temporal logic, Journal of the ACM 49, 672-713 (2002) · Zbl 1326.68181
[2] Arbab, F.: Reo: A channel-based coordination model for component composition, Mathematical structures in computer science 14, No. 3, 329-366 (2004) · Zbl 1085.68552 · doi:10.1017/S0960129504004153
[3] Arbab, F.; Baier, C.; De Boer, F.; Rutten, J. J. M.M.: Models and temporal logics for timed component connectors, , 198-207 (2004)
[4] 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, Lncs 3454 (2005)
[5] S. Azhar, G.L. Peterson, J.H. Reif, On multiplayer non-cooperative games of incomplete information: Part 1&2, Technical report, Durham, NC, USA, 1991
[6] Baier, C.; Sirjani, M.; Arbab, F.; Rutten, J. J. M.M.: Modeling component connectors in reo by constraint automata, Science of computer programming 61, 75-113 (2006) · Zbl 1105.68058 · doi:10.1016/j.scico.2005.10.008
[7] Tobias Blechmann, Joachim Klein, Sascha Klüppelholz, Vereofy. http://www.vereofy.de, 2008
[8] Chadha, Rhohid; Sistla, A. Prasad; Viswanathan, Mahesh: On the expressiveness of randomization in finite state monitors, , 18-29 (2008) · Zbl 1325.68128
[9] K. Chatterjee, L. Doyen, T.A. Henzinger, J.F. Raskin, Algorithms for omega-regular games with imperfect information. CoRR, abs/0706.2619, 2007 · Zbl 1125.91028
[10] Clarke, E. M.; Emerson, E. A.; Sistla, A. P.: Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM toplas 8, No. 2, 244-263 (1986) · Zbl 0591.68027
[11] De Alfaro, L.; Henzinger, T. A.: Interface automata, , 109-120 (2001)
[12] M. de Wulf, Laurent Doyen, Jean-François Raskin, A lattice theory for solving games of imperfect information, in: HSCC, 2006, pp. 153–168 · Zbl 1178.93072 · doi:10.1007/11730637
[13] Fischer, M. J.; Ladner, R. J.: Propositional dynamic logic of regular programs, Journal of computer and system science 8, 194-211 (1979) · Zbl 0408.03014 · doi:10.1016/0022-0000(79)90046-1
[14] Fitoussi, David; Tennenholtz, Moshe: Choosing social laws for multi-agent systems: minimality and simplicity, Artif. intell. 119, No. 1–2, 61-101 (2000) · Zbl 0945.68170 · doi:10.1016/S0004-3702(00)00006-0
[15] Francez, N.: Fairness, (1986) · Zbl 0602.68007
[16] R. Grosu, B. Rumpe, Concurrent timed port automata, Technical Report TUM-I9533, Techn. Univ. München, 1995. http://www4.informatik.tu-muenchen.de/reports/
[17] W. van der Hoek, M. Roberts, M. Wooldridge, Knowledge and social laws, in: AAMAS, 2005, pp. 674–681
[18] Van Der Hoek, W.; Wooldridge, M.: Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications, Studia logica 75, No. 1, 125-157 (2003) · Zbl 1034.03013 · doi:10.1023/A:1026185103185
[19] Klüppelholz, S.; Baier, C.: Symbolic model checking for channel-based component connectors, Science of computer programming 74, No. 9, 688-701 (2009) · Zbl 1167.68035 · doi:10.1016/j.scico.2008.09.020
[20] Lynch, N.; Tuttle, M. R.: An introduction to input/output automata, CWI quarterly 2, No. 3, 219-246 (1989) · Zbl 0677.68067
[21] Reif, J. H.: The complexity of two-player games of incomplete information, J. comput. Syst. sci. 29, No. 2, 274-301 (1984) · Zbl 0551.90100 · doi:10.1016/0022-0000(84)90034-5
[22] Jean-Guy Schneider, Markus Lumpe, Oscar Nierstrasz, Agent coordination via scripting languages, in: Coordination of Internet Agents: Models, Technologies, and Applications, 2001, pp. 153–175
[23] Schobbens, P. Y.: Alternating-time logic with imperfect recall, Entcs 85(2), 1-12 (2004) · Zbl 1270.68287
[24] P. Wolper, Specification and synthesis of communicating processes using an extended temporal logic, in: Proc. of POPL, 1982, pp. 20–33
[25] M. Wooldridge, Social laws in alternating time, in: DEON, 2004, p. 2 · Zbl 1169.68619
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.