VAS – Verification of Autonomous Systems

Note: Papers co-authored by group members before joining the group can be accessed from the authors’ individual web pages.

2012

• A. Griesmayer, Z. Liu, C. Morisset, S. Wang A Framework for Automated and Certified Refinement Steps (arXiv pre-print) accepted for publication, to appear in the Journal on Innovations in Systems and Software Engineering, 2012, Springer.
• P. Gonzalez, A. Griesmayer, A. Lomuscio. Verifying GSM-based Business Artifacts. To appear in the Proceedings of the 2012 IEEE International Conference on Web Services (ICWS2012). Honolulu, USA. pp 25-32. IEEE Press.
• W. Leister, J. Bjørk, R. Schlatte, E. B. Johnsen, A. Griesmayer. Exploiting Model Variability in ABS to Verify Distributed Algorithms. International Journal on Advances in Telecommunication, pp 55-68, Vol 5(1&2), 2012. IARIA Journals.
• F. Belardinelli, A. Lomuscio, F. Patrizi. An Abstraction Technique for the Verification of Artifact-Centric Systems. To appear in the Proceedings of the 13th International Conference Principles of Knowledge Representation and Reasoning (KR2012). Rome, Italy. AAAI Press.
• G. De Giacomo, P. Felli, A. Lomuscio. Synthesizing agent protocols from LTL specifications against multiple partially-observable environments.. To appear in the Proceedings of the 13th International Conference Principles of Knowledge Representation and Reasoning (KR2012). Rome, Italy. AAAI Press.
• F. Belardinelli, P. Gonzalez, A. Lomuscio. Automated Verification of Quantum Protocols using MCMAS. Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL12). Tallin, Estonia. Electronic Proceedings in Theoretical Computer Science. Vol 85, pp 48-62. Open Publishing Association.
• I. Boureanu, A.V. Jones, A. Lomuscio. Automatic Verification of Epistemic Specifications under Convergent Equational Theories. To Appear in the Proceedings of the 11th International Conferenceon Autonomous Agents and Multi-Agent systems (AAMAS12). Valencia,Spain. IFAAMAS Press.
• A.V. Jones, M. Knapik, A. Lomuscio, W. Penczek. Group Synthesis for Parametric Temporal-Epistemic Logic. To Appear in the Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS12). Valencia, Spain. IFAAMAS Press.

2011

• A. Lomuscio, H. Qu, M. Solanki. Towards verifying contract regulated service composition. Journal of Autonomous Agents and Multi-Agent Systems. pp 345-373, Vol 24(3), Springer.
• F. Belardinelli, A. Lomuscio, F. Patrizi. Verification of Deployed Artifact Systems via Data Abstraction. Proceedings of the 9th International Conference on Service Oriented Computing (ICSOC11). Paphos, Cyprus. Lecture Notes in Computer Science. Vol 7084, pp 142-156. Springer.
• F. Belardinelli, A.V. Jones, A. Lomuscio. Model checking temporal-epistemic logic using alternating tree automata. Fundamenta Informaticae. pp 19-37, Vol 112(1). A previous version of this paper appeared in the proceedings of the 13th International Workshop on Concurrency, Specification and Programming (CS&P10). Helenenau, Germany.
• F. Belardinelli, A. Lomuscio, F. Patrizi. A computationally grounded semantics for artifact centric systems and abstraction results. Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI11). Barcelona, Spain. pp 738-743. AAAI Press.
• J. Ezekiel, A. Lomuscio, L. Molnar,S. Veres. Verifying fault tolerance and self-diagnosability of an autonomous underwatervehicle. Poster Presentation. Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI11). Barcelona, Spain. pp 1659-1664. AAAI Press.
• A. Lomuscio, W. Penczek, M. Solanki, M. Szreter. Runtime monitoring of contract regulated web services. Fundamenta Informaticae. pp 339-355, Vol 111(3). A shorter version of this paper appeared as an extended abstract in the Proceedings of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS10). Toronto, Canada. pp 1149-1150, IFAAMAS Press.

2010

• J. Ezekiel, A. Lomuscio. A methodology for automatic diagnosability analysis. Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM10). Shanghai, China. Lecture Notes in Computer Science. Vol 6447 pp 549-564. Springer.
• A. Lomuscio, B. Strulo, N. Walker, P. Wu. Assume-Guarantee Reasoning with Local Specifications. Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM10). Shanghai, China. Lecture Notes in Computer Science. Vol 6447 pp 204-219. Springer.
• F. Belardinelli, A. Lomuscio. First-Order Linear-time Epistemic Logic Group Knowledge: An Axiomatisation of the Monodic Fragment. Fundamenta Informaticae. pp 175-190, Vol 106(1).
• A. Lomuscio, W. Penczek, H. Qu. Partial order reduction for model checking interleaved multi-agent systems. Fundamenta Informaticae. pp 71-90, Vol 101(1-2). A shorter versionof this paper appeared in the Proceedings of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS10). Toronto, Canada. pp 659-666. IFAAMAS Press.
• A. V. Jones, A. Lomuscio. Distributed BDD-based BMC for the Verification of Multi-Agent Systems. Fundamenta Informaticae. To appear. A shorter version of this paper appeared in the Proceedings of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS10). Toronto, Canada. pp 675-682, IFAAMAS Press.
• M. Cohen, A. Lomuscio. Non-elementary speedup for model checking synchronous perfect recall. Short paper. Proceedings of the 19th European Conference on Artificial Intelligence (ECAI10). Lisbon, Portugal. pp 1077-1078, IOS Press.
• M. Kwiatkowska, A. Lomuscio, H. Qu. Parallel Model Checking for Temporal Epistemic Logic. Proceedings of the 19th European Conference on Artificial Intelligence (ECAI10). Lisbon, Portugal. pp 543-548. IOS Press.
• A. Lomuscio, H. Qu, F. Russo. Automatic data abstraction in model checking Multi-Agent Systems. Proceedings of the 6th International Workshop on Model Checking and Artificial Intelligence (MochartVI). Atlanta, USA. pp 61-76.
• F. Belardinelli, A. Lomuscio. Interactions between knowledge and time in a first-order logic for multi-agent systems. Proceedings of the 12th International Conference on Knowledge Representation and Reasoning (KR10). Toronto, Canada. pp 38-48, AAAI Press.
• A. Lomuscio, B. Strulo, N. Walker, P. Wu. Model checking optimisation-based congestion control models. Fundamenta Informaticae. pp 77-96, Vol 102(1). A preliminary version of this paper appeared in the Proceedings of the 12th International Workshop on Concurrency, Specification and Programming (CS&P09). Krakow, Poland. pp 386-397. Warsaw University Press.
• I. Boureanu, M. Cohen, A. Lomuscio. Model checking detectability of attacks in multiagent systems. Proceedings of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS10). Toronto, Canada. pp 691-698, IFAAMAS Press.

2009

• I. Boureanu, M. Cohen, A. Lomuscio. A compilation method for the verification of temporal-epistemic properties of cryptographic protocols. Journal of Applied Non-Classical Logics. Vol 19(4), pp 463-487. A preliminary version of this paper appeared in the informal proceedings of the Joint International Workshop on Automated Reasoning for Security Protocols Analysis and Issues in the Theory of Security (ARSPA-WITS09). York, UK.
• J. Ezekiel, A. Lomuscio. An automated approach to verifying diagnosability in multi-agent systems. Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM09). Hanoi, Vietnam. pp 51-60. IEEE Press.
• M. Cohen, M. Dam, A. Lomuscio, H. Qu. A data symmetry reduction technique for temporal-epistemic logic. Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA09). Macao, SAR. China. Lecture Notes in Computer Science. Vol 5799 pp 69-83. Springer.
• M. Cohen, M. Dam, A. Lomuscio, H.Qu A Symmetry Reduction technique for model checking temporal epistemic logic. Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI09). Pasadena, USA. pp 721-726. AAAI Press.
• F. Belardinelli, A. Lomuscio. First-Order Linear-time Epistemic Logic Group Knowledge: An Axiomatisation of the Monodic Fragment. Proceedings of the 16th Workshop on Logic, Language, Information and Computation. Tokyo, Japan. Lecture Notes in Computer Science. Vol 5514 pp 140-154. Springer.
• A. Lomuscio, H. Qu, F. Raimondi MCMAS: A model checker for the verification of multi-agent systems. Proceedings of the 21th International Conference on Computer Aided Verification (CAV 2009). Grenoble, France. Lecture Notes in Computer Science. Vol 5643 pp 682-688. Springer.
• F. Belardinelli, A. Lomuscio. Quantified Epistemic Logic for reasoning about knowledge in Multi-Agent Systems. Artificial Intelligence.  Vol 173(9-10), pp 982-1013. Elsevier.
• A. Lomuscio, M. Solanki. Mapping OWL-S processes to multi agent systems: A verification oriented approach. Proceedings of the 6th European Semantic Web Conference (ESWC 2009). Lecture notes in Computer Science. Vol 5554 pp 578-592. Springer. (A previous version of this paper appeared in the Proceedings of the 4th International IEEE Workshop on Service Oriented Architectures in Converging Networked Environments (IEEE Press)).
• J. Ezekiel, A. Lomuscio. Combining fault injection and model checking to verify fault tolerance in multi-agent systems. Proceedings of the 8th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS09). Budapest, Hungary. pp 113-120. IFAAMAS Press.
• M. Cohen, M. Dam, A. Lomuscio, F. Russo Abstraction in model checking multi-agent systems . Proceedings of the 8th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS09). Budapest, Hungary. pp 945-952. IFAAMAS Press.

2008

• A. Lomuscio, H. Qu, M. Solanki. Towards verifying contract regulated service composition. Proceedings of the 8th International Conference on Web Services (ICWS08). Beijing, China. pp 255-261. IEEE Press.
• A. Lomuscio, H. Qu. Towards a partial order reduction techniques for model checking temporal epistemic logics. Proceedings of the 5th International Workshop on Model Checking and Artificial Intelligence (MochartV). Athens, Greece. Lecture Notes in Computer Computer Science. Vol 5348, pp 106-121. Springer.
• F. Belardinelli, A. Lomuscio. A complete quantified temporal epistemic logic. Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR08). Sydney, Australia. pp 705-714. AAAI Press.
• A. Lomuscio, W. Penczek. LDYIS: A framework for model checking security protocols. Fundamenta Informaticae, vol 85 (1-4), pp 359-375. IOS Press.
• A. Lomuscio, H. Qu,  M. Solanki. Towards verifying compliance in agent-based web service compositions. Proceedings of the 7th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS08). Estoril, Portugal. pp 265-272. IFAAMAS Press.

2007

• A. Lomuscio, W. Penczek, B. Wozna. Bounded model checking knowledge and real time. Artificial Intelligence. Vol 171(16-17), pp 1011-1038. Elsevier.
• A. Lomuscio, W. Penczek. Symbolic model checking for temporal epistemic logic. SIGACT News Logic Column. ACM SIGACT News. Logic Column. 38(3), pp 76-100. 2007. ACM Press.
• A. Lomuscio, W. Penczek. Model checking security protocols: a multiagent systems approach. Proceedings of the 10th International Workshop on Concurrency, Specification and Programming (CS&P07), pp 400-412. Warsaw University Press. An earlier version of this paper appeared as technical Report 1000. Polish Academia of Sciences. Warsaw.
• A. Lomuscio, H. Qu, M. Sergot, M. Solanki. Verifying Temporal Epistemic properties of Web service compositions. Proceedings of the 5th International Conference on Service Oriented Computing (ICSOC07). Vienna, Austria. Lecture Notes in Computer Science. Vol 4749, pp 456-461. Springer.
• F. Belardinelli, A. Lomuscio. A complete quantified epistemic logic for reasoning about message passing systems. Proceedings of the 8th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA VIII). Porto, Portugal.
• F. Belardinelli, A. Lomuscio. Quantified epistemic logics with flexible terms. A Meeting of the Minds: Proceedings of the Workshop on Logic, Rationality and Interaction. Beijing, China. J. van Benthem, S. Ju and F. Veltman editors. College Publications.
• S. Edelkamp, A. Lomuscio (editors). Proceedings of MoChartIV: 4th International Workshop on Model Checking and Artificial Intelligence. Springer LNCS Volume 4428.
• A. Lomuscio, F. Raimondi, B. Wozna. Verification of the Tesla protocol in MCMAS-X. Fundamenta Informaticae, vol 79 (3-4), pp 473-486. IOS Press.
• A. Lomuscio, B. Wozna. A temporal epistemic logic with a reset operation. Proceedings of the 6th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS07). Honolulu, USA. IFAAMAS Press.
• F. Belardinelli, A. Lomuscio. A quantified epistemic logic for reasoning about multi-agent systems. Proceedings of the 6th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS07). Short paper. Honolulu, USA. IFAAMAS Press.
• A. Lomuscio, C. Pecheur, F. Raimondi. Verification of knowledge and time with NuSMV. Proceedings of the 20th International Conference on Artificial Intelligence (IJCAI07), Hyderabadad, India.

2006

• A. Lomuscio, F. Raimondi. The complexity of model checking concurrent programs against CTLK specifications. Post-proceedings of the 4th workshop on Declarative Agent Languages and Technologies (DALT06), Springer LNCS Vol 4327, pp 29-42.
• A. Lomuscio, F. Raimondi, B. Wozna. Verification of the TESLA protocol with MCMAS-X. Proceedings of CS&P, International Workshop on Concurrency, Specification and Programming. Wandlitz, Germany, September 2006. Humboldt University.
• A. Lomuscio, B. Wozna, A. Zbrzezny. Bounded model checking real-time multi-agent systems with clock differences: theory and implementation. Proceedings of the 4th International Workshop on Model Checking and Artificial Intelligence (MochartIV).  LNCS Springer Volume 4428.
• A. Lomuscio, B. Wozna. A complete and decidable axiomatisation of deontic interpreted systems. Proceedings of the 8th International Workshop on application of Deontic Logic to Computer Science (DEON06). Utrecht, Netherlands. Springer LNCS Vol 4048.
• W. van der Hoek, A. Lomuscio, E. de Vink, M. Wooldridge editors. Proceedings of LCMAS3, Workshop on Logic and Communication in Multi-Agent Systems. Electronic lecture notes in Theoretical Computer Science. Volume 157:4. Elsevier.
• M. Kacprzak, A. Lomuscio, A. Niewiadomski, W. Penczek,F. Raimondi, M. Szreter. Comparing BDD and SAT based techniques for model checking Chaum’s Dining cryptography protocol. Fundamenta Informaticae. Vol 72. pp 215–234. IOS Press.
• A. Lomuscio, F. Raimondi. The complexity of model checking concurrent programs against CTLK specifications. Proceedings of 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06). Short Paper. Hakodate, Japan. ACM Press.
• A. Lomuscio, F. Raimondi. Model checking knowledge, strategies, and games in multi-agent systems. Proceedings of the 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06). Hakodate, Japan. ACM Press.
• W. van der Hoek, A. Lomuscio, M. Wooldridge. On the complexity of practical ATL model checking knowledge, strategies, and games in multi-agent systems. Proceedings of the 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06). Hakodate, Japan. ACM Press.
• A. Lomuscio, B. Wozna. A complete and decidable security-specialised logic and its application to the TESLA protocol. Proceedings of the 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06). Hakodate, Japan. ACM Press.
• A. Lomuscio, F. Raimondi. MCMAS: a tool for verifying multi-agent systems. Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS06). Vienna, Austria. Springer LNCS Vol 3920, pp 450-454.