The computational complexity of scenario-based agent verification and design

Amyot, 2003, An evaluation of scenario notations for telecommunication systems development, Telecomm. Syst. J., 24, 61, 10.1023/A:1025890110119 R. Alur, R. Grosu, M. McDougall, Modular refinement of hierarchic reactive machines, in: Proc. of POPL'00, the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, MA, 2000. ACM SIGPLAN-SIGACT Abadi, 1989, Realizable and unrealizable specifications of reactive systems, vol. 372 Bohn, 2002, Modeling and validating train system applications using statemate and live sequence charts Bordini, 2003, Model checking agent speak, 409 A. Bunker, G. Gopalakrishnan, Verifying a virtual component interface-based PCI bus wrapper using an LSC-based specification, Technical Report UUCS-02-004, University of Utah, School of Computing, 2002 Bontemps, 2004, As fast as sound (lightweight formal scenario synthesis and verification), 27 Bontemps, 2003, Applying LSCs to the specification of an air traffic control system Büchi, 1969, Solving sequential conditions finite-state strategies, Trans. Amer. Math. Soc., 138, 295, 10.1090/S0002-9947-1969-0280205-0 Y. Bontemps, Automated verification of state-based specifications against scenarios (a step towards relating inter-object to intra-object specifications), Master's thesis, University of Namur, Namur, Belgium, 2001 Y. Bontemps, Realizability of scenario-based specifications, Diplôme d'études approfondies, Facultés Universitaires Notre-Dame de la Paix, Institut d'Informatique, University of Namur, Computer Science Department, Namur, Belgium, 2003 Y. Bontemps, On the semantics of uml 2.0 interaction diagram, Technical report, University of Namur, Institut d'Informatique, 2004 Y. Bontemps, Relating inter-agent and intra-agent specifications (the case of live sequence charts), PhD thesis, Facultés Universitaires Notre-Dame de la Paix, Institut d'Informatique, University of Namur, Computer Science Department, 2005 Bontemps, 2004, Synthesis of open reactive systems from scenario-based specifications, Fundamenta Informaticae, 62, 139 A. Church, Logic, arithmetic and automata, in: Proc. of Intern. Cong. Math., 1963, pp. 23–35 M. Victoria e Cengarle, A. Knapp, Uml 2.0 interactions: Semantics and refinement, in: J. Jürjens, E.B. Fernandez, R. France, B. Rumpe, (Eds.), Proc. of 3rd Int. Wsh. Critical Systems Development with UML (CSDUML'04, Proceedings), 2004, pp. 85–99 Chandra, 1981, Alternation, J. ACM, 28, 114, 10.1145/322234.322243 Damm, 2001, LSCs: Breathing life into message sequence charts, Formal Methods Syst. Design, 19, 45, 10.1023/A:1011227529550 Dunne, 2003, Complexity results for agent design problems, Ann. Math. Comput. Teleinform., 1, 19 E.A. Emerson, Temporal and modal logic, in: [56], Chapter 16, pp. 997–1072, ISBN 0-262-72015-9, second printing, 1998 Esteva, 2001, On the formal specification of electronic institutions, vol. 1991, 126 P. Gastin, B. Lerman, M. Zeitoun, Distributed games and distributed control for asynchronous systems, in: Proc. of Latin American Theoretical Informatics (LATIN'04), 2004 Harel, 1987, Statecharts: a visual formalism for complex systems, Sci. Comput. Programming, 8, 231, 10.1016/0167-6423(87)90035-9 Harel, 2001, From play-in scenarios to code: an achievable dream, IEEE Comput., 34, 53, 10.1109/2.895118 Harel, 2002, Synthesizing state-based object systems from LSC specifications, Internat. J. Foundations of Computer Science, 13, 5, 10.1142/S0129054102000935 Harel, 2003 Holzmann, 1997, The model checker SPIN, Software Engrg., 23, 279, 10.1109/32.588521 Huget Harel, 2002, On the complexity of verifying concurrent transition systems, Inform. and Comput., 173, 10.1006/inco.2001.2920 Huget, 2003, Model checking for acl compliance verification N. Kam, D. Harel, H. Kugler, R. Marelly, A. Pnueli, E.J.A. Hubbard, M.J. Stern, Formal modeling of c. elegans development: a scenario-based approach, in: Proc. CMSB 2003, 2003, pp. 4–20 Kugler, 2005, Temporal logic for live sequence charts Kirsten, 2002, Alternating Tree Automata and Parity Games, vol. 2500 O. Kupferman, M.Y. Vardi, Synthesizing distributed systems, in: Proc. 16th IEEE Symp. on Logic in Computer Science, 2001 Lynch, 1989, An introduction to input/output automata, CWI Quarterly, 2, 219 M. Maidl, The common fragment of CTL and LTL, in: Proc. 41st Annual Symposium on Foundations of Computer Science, 2000, pp. 643–652 R. Marelly, D. Harel, H. Kugler, Multiple instances and symbolic variables in executable sequence charts, in: Proc. 17th Ann. ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'02), Seattle, WA, 2002, pp. 83–100 A. Muscholl, D. Peled, Z. Su, Deciding properties of message sequence charts, Foundations of Software Science and Computer Structures (1998) Madhusudhan, 2002, A decidable class of asynchronous distributed controllers, vol. 2421 Papadimitriou, 1994 Peled, 2000 A. Pnueli, R. Rosner, On the synthesis of a reactive module, in: Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989, pp. 179–190 Pnueli, 1989, On the synthesis of an asynchronous reactive module, vol. 372, 652 R. Rosner, Modular synthesis of reactive systems, PhD thesis, The Weizmann Institute of Science, Rehovot, Israel, 1992 Russell, 1995, Provably bounded-optimal agents, J. Artificial Intelligence Res., 2, 575, 10.1613/jair.133 Savitch, 1970, Relationships between nondeterministic and deterministic tape complexities, J. Comput. System Sci., 4, 177, 10.1016/S0022-0000(70)80006-X Prasad Sistla, 1985, Complexity of propositional temporal logics, J. ACM, 32, 733, 10.1145/3828.3837 Stewart, 2003, The complexity of achievement and maintenance problems in agent-based systems, Artificial Intelligence, 146, 175, 10.1016/S0004-3702(03)00014-6 W. Thomas, Automata on infinite objects, in: [56], Chapter 4, pp. 134–191. ISBN 0-262-72015-9 (second printing, 1998) Thomas, 1997, Languages, automata, and logic Tripakis, 2004, Undecidable problems of decentralized observation and control on regular languages, Inform. Process. Lett., 90, 10.1016/j.ipl.2004.01.004 Vardi, 1995, An automata-theoretic approach to fair realizability and synthesis, 267 1990 Vardi, 1986, Automata-theoretic techniques for modal logics of programs, J. Comput. System Sci., 32, 183, 10.1016/0022-0000(86)90026-7 C.D. Walton, Multi-agent dialogue protocols, in: Proceedings of the 8th International Symposium on Artificial Intelligence and Mathematics, Ft. Lauderdale, FL, 2004 Wooldridge, 2002, The computational complexity of agent verification, vol. 2333, 115 Wooldridge, 2002, Model checking multi-agent systems with mable, 952 Wolper, 1983, Temporal logic can be more expressive, Inform. and Control, 56, 72, 10.1016/S0019-9958(83)80051-5