@article(DBLP:journals/fmsd/AlurH99b,
 author       = "R. Alur and T. A. Henzinger",
 year         = "1999",
 title        = "Reactive Modules",
 journal      = "Formal Methods in System Design",
 volume       = "15",
 number       = "1",
 pages        = "7--48",
 doi          = "10.1023/A:1008739929481",
)
@article(Alur02ATL,
 author       = "R. Alur and T. A. Henzinger and O. Kupferman",
 year         = "2002",
 title        = "{A}lternating-Time {T}emporal {L}ogic",
 journal      = "Journal of the ACM",
 volume       = "49",
 pages        = "672--713",
 doi          = "10.1145/585265.585270",
)
@inproceedings(Alur99communicatingHSM,
 author       = "R. Alur and S. Kannan and M. Yannakakis",
 year         = "1999",
 title        = "Communicating Hierarchical State Machines",
 booktitle    = "Proceedings of ICALP",
 pages        = "169--178",
 doi          = "10.1007/3-540-48523-6\_14",
)
@phdthesis(Calta12phd,
 author       = "J. Calta",
 year         = "2012",
 title        = "Synthesis of Strategies for Multi-Agent Systems",
 school       = "Humboldt University Berlin",
)
@article(Chaum,
 author       = "D. Chaum",
 year         = "1988",
 title        = "The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability",
 journal      = "Journal of Cryptology",
 volume       = "1(1)",
 pages        = "65--75",
 doi          = "10.1007/BF00206326",
)
@incollection(Dembinski03verics,
 author       = "P. Dembi\'nski and A. Janowska and P. Janowski and W. Penczek and A. P\'o{\l }rola and M. Szreter and B. Wo\'zna and A. Zbrzezny",
 year         = "2003",
 title        = "Verics: A Tool for Verifying Timed Automata and Estelle Specifications",
 booktitle    = "Proceedings of the of the 9th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03)",
 series       = "LNCS",
 volume       = "2619",
 publisher    = "Springer",
 pages        = "278--283",
 doi          = "10.1007/3-540-36577-X\_20",
)
@incollection(Emerson90temporal,
 author       = "E. A. Emerson",
 year         = "1990",
 title        = "Temporal and Modal Logic",
 editor       = "J. van Leeuwen",
 booktitle    = "Handbook of Theoretical Computer Science",
 volume       = "B",
 publisher    = "Elsevier Science Publishers",
 pages        = "995--1072",
)
@book(Fagin95knowledge,
 author       = "R. Fagin and J. Y. Halpern and Y. Moses and M. Y. Vardi",
 year         = "1995",
 title        = "Reasoning about Knowledge",
 publisher    = "MIT Press",
)
@inproceedings(DBLP:conf/concur/FisherHNPSV11,
 author       = "J. Fisher and T. A. Henzinger and D. Nickovic and N. Piterman and A. V. Singh and M. Y. Vardi",
 year         = "2011",
 title        = "Dynamic Reactive Modules",
 booktitle    = "Proceedings of CONCUR",
 pages        = "404--418",
 doi          = "10.1007/978-3-642-23217-6\_27",
)
@book(Gecseg86automata,
 author       = "F. Gecseg",
 year         = "1986",
 title        = "Products of Automata",
 series       = "EATCS Monographs on Theor. Comput. Sci.",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-61611-2",
)
@article(Holzmannn97spin,
 author       = "G. J. Holzmannn",
 year         = "1997",
 title        = "The Model Checker {SPIN}",
 journal      = "IEEE Transactions on Software Engineering",
 volume       = "23",
 number       = "5",
 pages        = "279--295",
 doi          = "10.1109/32.588521",
)
@techreport(Jamroga06mis-tr,
 author       = "W. Jamroga and T. {\r A}gotnes",
 year         = "2006",
 title        = "Modular Interpreted Systems: A Preliminary Report",
 type         = "Technical Report",
 number       = "IfI-06-15",
 institution  = "Clausthal University of Technology",
)
@inproceedings(Jamroga07mis-aamas,
 author       = "W. Jamroga and T. {\r A}gotnes",
 year         = "2007",
 title        = "Modular Interpreted Systems",
 booktitle    = "Proceedings of AAMAS'07",
 pages        = "892--899",
 doi          = "10.1145/1329125.1329286",
)
@inproceedings(Koester11abstraction,
 author       = "M. K{\"o}ster and P. Lohmann",
 year         = "2011",
 title        = "Abstraction for model checking modular interpreted systems over {ATL}",
 booktitle    = "Proceedings of AAMAS",
 pages        = "1129--1130",
)
@article(Laroussinie08expATL,
 author       = "F. Laroussinie and N. Markey and G. Oreiby",
 year         = "2008",
 title        = "On the Expressiveness and Complexity of {ATL}",
 journal      = "Logical Methods in Computer Science",
 volume       = "4",
 pages        = "7",
 doi          = "10.2168/LMCS-4(2:7)2008",
)
@inproceedings(Lichtenstein85checking,
 author       = "O. Lichtenstein and A. Pnueli",
 year         = "1985",
 title        = "Checking that finite state concurrent programs satisfy their linear specification",
 booktitle    = "POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "97--107",
 doi          = "10.1145/318593.318622",
)
@inproceedings(Lomuscio06mcmas,
 author       = "A. Lomuscio and F. Raimondi",
 year         = "2006",
 title        = "{MCMAS} : A Model Checker for Multi-agent Systems",
 booktitle    = "Proceedings of TACAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "4314",
 pages        = "450--454",
 doi          = "10.1007/11691372\_31",
)
@inproceedings(Murano08hierarchical,
 author       = "A. Murano and M. Napoli and M. Parente",
 year         = "2008",
 title        = "Program Complexity in Hierarchical Module Checking",
 booktitle    = "Proceedings of LPAR",
 pages        = "318--332",
 doi          = "10.1007/978-3-540-89439-1\_23",
)
@phdthesis(Raimondi06phd,
 author       = "F. Raimondi",
 year         = "2006",
 title        = "Model Checking Multi-Agent Systems",
 school       = "University College London",
)
@article(Torre08HSM,
 author       = "S. La Torre and M. Napoli and M. Parente and G. Parlato",
 year         = "2008",
 title        = "Verification of scope-dependent hierarchical state machines",
 journal      = "Information and Computation",
 volume       = "206",
 number       = "9-10",
 pages        = "1161--1177",
 doi          = "10.1016/j.ic.2008.03.017",
)