Publications

P. Kouvaros, F. Leofante, B. Edwards, C. Chung, D. Margineantu, A. Lomuscio.
Verification of Semantic Key Point Detection for Aircraft Pose Estimation.
Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning (KR23). Rhodes, Greece. AAAI Press.

F. Leofante, P. Henriksen, A. Lomuscio.
Verification-friendly Networks: the Case for Parametric ReLUs.
Proceedings of the 36th International Conference on Neural Networks (IJCNN23). Gold Coast, Australia. IEEE Press.

H. Hanspal, A. Lomuscio.
Efficient Verification of Neural Networks against LVM-based Specifications.
Proceedings of the 36th IEEE Conference on Computer Vision and Pattern Recognition (CVPR23).

M. Hosseini, A. Lomuscio.
Bounded and Unbounded Verification of RNN-Based Agents in Non-deterministic Environments (extended abstract).
Proceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS23). London, UK. IFAAMAS Press.

F. Leofante, A. Lomuscio.
Towards Robust Contrastive Explanations for Human-Neural Multi-Agent Systems (extended abstract).
Proceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS23). London, UK. IFAAMAS Press.

J. Lan, B. Brueckner, A. Lomuscio.
A Semidefinite Relaxation based Branch-and-Bound Method for Tight Neural Network Verification.
Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA.

J. Lan, Y. Zheng, A. Lomuscio.
Iteratively Enhanced Semidefinite Relaxations for Efficient Neural Network Verification.
Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA.

P. Henriksen, A. Lomuscio.
Robust Training of Neural Networks against Bias Field Perturbations.
Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA.

E. Pirovano, A. Lomuscio.
A Counter Abstraction Technique for Verifying Properties of Probabilistic Swarm Systems.
Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA. Journal Track.

F. Belardinelli, A. Lomuscio, V. Malvone, E. Yu.
Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications
Journal of Artificial Intelligence Research.

A. Lomuscio and E. Pirovano.
A Counter Abstraction Technique for Verifying Properties of Probabilistic Swarm Systems
Artificial Intelligence. Elsevier.

P. Henriksen, F. Leofante, A. Lomuscio.
Repairing Misclassifications in Neural Networks Using Limited Data.
Proceedings of the 37th ACM/SIGAPP Symposium On Applied Computing (SAC22). Virtual Conference.

J. Lan, Y. Zheng, A. Lomuscio.
Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations
Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI22). Virtual Conference.

M. Akintunde, E. Botoeva, P. Kouvaros, A. Lomuscio.
Formal Verification of Neural Agents in Non-deterministic Environments.
Journal of Autonomous Agents and Multi-Agent Systems, Vol 36(1). Springer.

V. Hashemi, P. Kouvaros, A. Lomuscio.
OSIP: Tightened Bound Propagation for the Verification of ReLU Neural Networks.
Proceedings of the 19th International Conference on Software Engineering and Formal Methods (SEFM21). Virtual Conference.

Y-L. Liu, A. Lomuscio.
Robustness Learning via Decision Tree Search Robust Optimisation.
Proceedings of the 31st British Machine Vision Conference (BMVC21). Virtual Conference.

P. Henriksen, K. Hammernik, D. Rueckert, A. Lomuscio.
Bias Field Robustness Verification of Large Neural Image Classifiers.
Proceedings of the 31st British Machine Vision Conference (BMVC21). Virtual Conference.

P. Kouvaros, T. Kyono, F. Leofante, A. Lomuscio, D. Margineantu, D. Osipychev, Y. Zheng.
Formal Analysis of Neural Network-based Systems in the Aircraft Domain.
Proceedings of the 24th International Symposium on Formal Methods (FM21). Virtual conference.

B. Aminof, G. De Giacomo, A. Lomuscio, A. Murano, S. Rubin.
Synthesizing Best-effort Strategies under Multiple Environment Specifications.
Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR21). Hanoi, Vietnam. AAAI Press.

B. Batten, P. Kouvaros, A. Lomuscio, Y. Zheng.
Efficient Neural Network Verification via Layer-based Semidefinite Relaxations and Linear Cuts.
Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Montreal, Canada.

F. Belardinelli, S. Knight, A. Lomuscio, B. Maubert, N. Murano, S. Rubin.
Reasoning about agents that may know other agents’ strategies.
Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Montreal, Canada.

P. Henriksen, A. Lomuscio.
DEEPSPLIT: An Efficient Splitting Method for Neural Network Verification via Indirect Effect Analysis.
Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Montreal, Canada.

P. Kouvaros, A. Lomuscio.
Towards Scalable Complete Verification of ReLU Neural Networks via Dependency-based Branching.
Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Montreal, Canada.

F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin.
Verification of multi-agent systems with public actions against strategy logic.
Artificial Intelligence. Elsevier.

A. Lomuscio, E. Pirovano.
Verifying Fault-Tolerance in Probabilistic Swarm Systems.
Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI-PRICAI20). Yokohama, Japan. AAAI Press.

B. Aminof, G. De Giacomo, A. Lomuscio, A. Murano, S. Rubin.
Synthesizing best-effort strategies under expected and exceptional environment behaviors.
Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI-PRICAI20). Yokohama, Japan. AAAI Press.

Y-L. Liu, A. Lomuscio.
MRobust: A Method for Robustness against Adversarial Attacks on Deep Neural Networks.
Proceedings of the 33rd International Conference on Neural Networks (IJCNN20). Edinburgh, UK. IEEE Press.

P. Henriksen, A. Lomuscio.
Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search.
Proceedings of the 24th European Conference on Artificial Intelligence (ECAI20). Santiago de Compostela, Spain.

M. Akintunde, E. Botoeva, P. Kouvaros, A. Lomuscio.
Formal Verification of Neural Agents in Non-Deterministic Environments. (video talk)
Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Auckland, New Zealand. IFAAMAS Press.

M. Akintunde, E. Botoeva, P. Kouvaros, A. Lomuscio.
Verifying Strategic Abilities of Neural Multi-agent Systems.
Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR20). Virtual conference. AAAI Press.

A. Lomuscio, E. Pirovano.
Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems. (video talk)
Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Auckland, New Zealand. IFAAMAS Press.

E. Botoeva, P. Kouvaros, J. Kronqvist, A. Lomuscio, R. Misener.
Efficient Verification of Neural Networks via Dependency Analysis.
Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20). New York City, New York. AAAI Press.

F. Belardinelli, A. Lomuscio, E. Yu.
Model Checking Temporal Epistemic Logic under Bounded Recall.
Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20). New York City, New York. AAAI Press.

Y-L. Liu, A. Lomuscio.
An MCTS-based Adversarial Training Method for Image Recognition
Proceedings of the 32nd International Conference on Neural Networks (IJCNN19). Budapest, Hungary. IEEE Press.

P. Kouvaros, A. Lomuscio, E. Pirovano, H. Punchihewa.
Formal Verification of Open Multi-Agent Systems
Proceedings of the 18th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS19). Montreal, Canada. IFAAMAS Press.

A. Lomuscio, E. Pirovano.
A Counter Abstraction Technique for the Verification of Probabilistic Swarm Systems
Proceedings of the 18th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS19). Montreal, Canada. IFAAMAS Press.

F. Belardinelli, A. Lomuscio, V. Malvone.
An Abstraction-based Method for Verifying Strategic Properties in Multi-agent Systems with Imperfect Information
Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI 2019). Honolulu, Hawaii. AAAI Press.

M. Akintunde, A. Kevorchian, A. Lomuscio, E. Pirovano
Verification of RNN-Based Neural Agent-Environment Systems
Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI 2019). Honolulu, Hawaii. AAAI Press.

F. Belardinelli, A. Lomuscio, V. Malvone.
Approximating Perfect Recall when Model Checking Strategic Abilities
Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR18). Tempe, Arizona. AAAI Press.

M. Akintunde, A. Lomuscio, L. Maganti, E. Pirovano
Reachability Analysis for Neural Agent-Environment Systems
Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR18). Tempe, Arizona. AAAI Press.

P. Kouvaros, A. Lomuscio, E. Pirovano.
Symbolic Synthesis of Fault-Tolerance Ratios in Parameterised Multi-Agent Systems
Proceedings of the 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI18). Stockholm, Sweden. AAAI Press.

A. Lomuscio, E. Pirovano.
Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems
Proceedings of the 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI18). Stockholm, Sweden. AAAI Press.

F. Belardinelli, A. Lomuscio, N. Murano, S. Rubin.
Alternating-time Temporal Logic on Finite Traces
Proceedings of the 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI18). Stockholm, Sweden. AAAI Press.

A. Lomuscio, M. Y. Vardi (eds).
Introduction to Special Issue on Strategic Reasoning
Information and Computation. 2018. (Extended versions of selected articles from the 4th International Workshop on Strategic Reasoning, New York, USA, 2016).

J. Kong, A. Lomuscio.
Model Checking Multi-Agent Systems against LDLK Specifications on Finite Traces
Proceedings of the 17th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS18). Stockholm, Sweden. IFAAMAS Press.

F. Belardinelli, A. Lomuscio, N. Murano. S. Rubin.
Decidable Verification of Multi-agent Systems with Bounded Private Actions
(extended abstract). Proceedings of the 17th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS18). Stockholm, Sweden. IFAAMAS Press.

P. Kouvaros, A. Lomuscio.
Towards the Formal Verification of Correctness and Robustness of Robot Swarms (Invited Talk).
Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic.

A. Lomuscio, L. Maganti.
An approach to reachability analysis for feed-forward ReLU neural Networks
arXiv preprint. arXiv:1706.07351 [cs.AI].

P. Cermak, A. Lomuscio, F. Mogavero, A. Murano.
Practical Verification of Multi-Agent Systems against SLK Specifications
Information and Computation.

P. Kouvaros, A. Lomuscio.
Verifying Fault-tolerance in Parameterised Multi-Agent Systems
Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 288-294. AAAI Press.

J. Kong, A. Lomuscio.
Model Checking Multi-Agent Systems against LDLK Specifications
Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 1138-1144. AAAI Press.

F. Belardinelli, A. Lomuscio, N. Murano. S. Rubin.
Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic
Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 91-97. AAAI Press.

F. Belardinelli, P. Kouvaros, A. Lomuscio.
Parameterised Verification of Data-aware Multi-agent Systems.
Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. pp 98-104. AAAI Press.

R. Hasani, D Haerle, C. Baumgartner, A. Lomuscio, R Grosu.
Compositional Neural-Network Modeling of Complex Analog Circuits.
Proceedings of the 30th International Conference on Neural Networks (IJCNN17). Anchorage, USA. pp 2235-2242. IEEE Press.

J. Kong, A. Lomuscio.
Symbolic Model Checking Multi-Agent Systems against CTL*K Specifications
Proceedings of the 16th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS17). Sao Paolo, Brazil. pp 114-122. IFAAMAS Press.

F. Belardinelli, A. Lomuscio.
Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect Information
Proceedings of the 16th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS17). Sao Paolo, Brazil. pp 1259-1267. IFAAMAS Press.

F. Belardinelli, A. Lomuscio, N. Murano. S. Rubin.
Verification of Multi-agent Systems with Imperfect Information and Public Actions
Proceedings of the 16th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS17). Sao Paolo, Brazil. pp 1268-1276. IFAAMAS Press.

P. Kouvaros, A. Lomuscio.
Parameterised Verification of Infinite State Multi-Agent Systems via Predicate Abstraction
Proceedings of the 31th AAAI Conference on Artificial Intelligence (AAAI17). San Francisco (CA), USA. pp 3013-3020. AAAI Press.

A. Lomuscio, H. Qu, F. Raimondi
MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems
International Journal on Software Tools for Technology Transfer. Vol 19(1); pp 9–30. Springer. 2017.

F. Belardinelli, A. Lomuscio.
A Three-value Abstraction Technique for the Verification of Epistemic Properties in Multi-agent Systems
Proceedings of the 15th European Conference on Logics in Artificial Intelligence (JELIA16). Larnaca, Cyprus. Lecture Notes in Computer Science. Vol 10021, pp 112-126. Springer.

A. Lomuscio, M. Y. Vardi, eds.
Proceedings of the 4th International Workshop on Strategic Reasoning (SR2016)
New York, USA.

P. Kouvaros, A. Lomuscio.
Parameterised Model Checking for Alternating-time Temporal Logic
Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands.

F. Belardinelli, A. Lomuscio.
Abstraction-based Verification of Infinite-state Reactive Modules
Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands.

F. Belardinelli, A. Lomuscio, J. Michaliszyn.
Agent-based Refinement for Predicate Abstraction of Multi-Agent Systems.
Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands.

P. Kouvaros, A. Lomuscio.
Formal Verification of Opinion Formation in Swarms
Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. IFAAMAS Press.

I. Boureanu, P. Kouvaros, A. Lomuscio.
Verifying Security Properties in Unbounded Multiagent Systems
Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. IFAAMAS Press.

A. Lomuscio, J. Michaliszyn.
Verification of Multi-Agent Systems via Predicate Abstraction against ATLK specifications
Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. IFAAMAS Press.

A. Lomuscio, J. Michaliszyn.
Model Checking Multi-Agent Systems against Epistemic HS Specifications with Regular Expressions
Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR16). Cape Town, South Africa. AAAI Press.

P. Kouvaros, A. Lomuscio.
Parameterised Verification for Multi-Agent Systems
Artificial Intelligence. Elsevier.

P. Gonzalez, A. Griesmayer, A. Lomuscio.
Verification of GSM-based Artifact-centric Systems by Predicate Abstraction
Proceedings of the 13th International Conference on Service Oriented Computing (ICSOC15). Goa, India.

P. Kouvaros, A. Lomuscio.
Verifying Emergent Properties of Swarms
Proceedings of the Twenty-Fourth International Conference on Artificial Intelligence (IJCAI15). Buonos Aires, Argentina. AAAI Press.

F. Belardinelli, D. Grossi, A. Lomuscio.
Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems
Proceedings of the Twenty-Fourth International Conference on Artificial Intelligence (IJCAI15). Buonos Aires, Argentina. AAAI Press.

A. Lomuscio, H. Qu, F. Raimondi
MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems
International Journal on Software Tools for Technology Transfer.

A. Lomuscio, W. Penczek. Model Checking Temporal Epistemic Logic. Chapter 8 of the
Handbook of Epistemic Logic
H. van Ditmarsch, J. Halpern, W. van der Hoek, and B. Kooi (eds.). College Publications, pp 397-441.

A. Lomuscio, J. Michaliszyn.
Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions.
Proceedings of the 14th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS15). Istanbul, Turkey. IFAAMAS Press.

A. Lomuscio, H. Paquet.
Verification of Multi-Agent Systems via SDD-based Model Checking (Extended Abstract)
Proceedings of the 14th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS15). Istanbul, Turkey. IFAAMAS Press.

P. Kouvaros, A. Lomuscio.
A Counter Abstraction Technique for the Verification of Robot Swarms
Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI15). Austin, Texas. pp 2081-2088. AAAI Press.

P. Cermak, A. Lomuscio, A. Murano.
Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications
Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI15). Austin, Texas. pp 2038-2044. AAAI Press.

F. Belardinelli, A. Lomuscio, F. Patrizi.
Verification of Agent-based Artifact Systems
Journal of Artificial Intelligence Research. Vol 51, pp 333–376. AAAI Press.

A. Lomuscio, J. Michaliszyn.
Decidability of model checking multi-agent systems against some EHS specifications
Proceedings of the 21st European Conference on Artificial Intelligence (ECAI14). Prague, Czech Republic, pp 543-548. IOS Press.

A. Lomuscio, P. Scerri, A. Bazzan, M. Huhns (Eds.).
Proceedings of the 13th International Conference on Autonomous Agents and Multiagent Systems
(AAMAS14). IFAAMAS Press.

A. Lomuscio, S. Nepal, F. Patrizi, B. Benatallah, I. Brandic (Eds.).
Proceedings of the Satellite Events of the 11th International Conference on Service Oriented Computing
(ICSOC14). LNCS Vol 8377. Springer.

P. Cermak, A. Lomuscio, F. Mogavero, A. Murano.
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
Proceedings of the 26th International Conference on Computer Aided Verification (CAV14). Vienna, Austria. pp 525-532. Springer

A. Lomuscio, J. Michaliszyn.
Model Checking Unbounded Artifact-Centric Systems
Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR14), Vienna, Austria. pp 488-497. AAAI Press.

A. Lomuscio, J. Michaliszyn.
An abstraction technique for the verification of multi-agent systems against ATL specifications
Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR14), Vienna, Austria. pp 428-437. AAAI Press.

P. Gonzalez, A. Griesmayer, A. Lomuscio.
Model checking GSM-based Multi-Agent systems
Proceedings of the Satellite Events of the 11th International Conference on Service Oriented Computing. LNCS Vol 8377. pp 54-68. Springer. A previous version of this paper appeared in the Proceedings of the 9th International Workshop on Automated Specification and Verification of Wed Services (WWV13). Florence, Italy.

A. Lomuscio, J. Michaliszyn.
An Epistemic Halpern-Shoham Logic
Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13). Beijing, China. pp 1010-1016. AAAI Press.

F. Belardinelli, A. Lomuscio.
Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems
Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13). Beijing, China. pp 725-731. AAAI Press.

P. Kouvaros, A. Lomuscio.
A Cutoff Technique for the Verification of Parameterised Interpreted Systems with Parameterised Environments
Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13). pp 2013-2019. AAAI Press.

A. Griesmayer, A. Lomuscio.
Model Checking Distributed Systems against Temporal-Epistemic Specifications
Proceedings of the IFIP Joint International Conference on Formal Techniques for Distributed Systems (FORTE/FMOODS). Florence, Italy. LNCS Vol 7892. pp 130-145. Springer.

P. Kouvaros, A. Lomuscio.
Automatic Verification of Parametrised Interleaved Multi-Agent Systems
Proceedings of the 12th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS13). Saint Paul, MN, USA. pp 861-868. IFAAMAS Press.

A. Lomuscio, B. Strulo, N. Walker, P. Wu.
Assume-Guarantee Reasoning with Local Specifications
International Journal of Foundations of Theoretical Computer Science, Vol 24(4). pp 419-444. An earlier version of this paper appeared in the Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM10). Shanghai, China. LNCS Vol 6447. pp 204-219. Springer.

F. Belardinelli, A. Lomuscio.
Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results
Journal of Artificial Intelligence Research, Vol 45. pp 1-45.

F. Belardinelli, A. Lomuscio, F. Patrizi.
Verification of GSM-based artifact-centric systems through finite abstraction
Proceedings of the 10th International Conference on Service Oriented Computing (ISCOC12). Shanghai, China. Lecture Notes in Computer Science, Vol 7636. pp 17-31. Springer.

A. Griesmayer, Z. Liu, C. Morisset, S. Wang
A Framework for Automated and Certified Refinement Steps (arXiv pre-print)
accepted for publication in the Journal on Innovations in Systems and Software Engineering, 2012, Springer.

P. Gonzalez, A. Griesmayer, A. Lomuscio.
Verifying GSM-based Business Artifacts
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 Vol 5(1&2). pp 55-68. ARIA Journals.

F. Belardinelli, A. Lomuscio, F. Patrizi.
An Abstraction Technique for the Verification of Artifact-Centric Systems
Proceedings of the 13th International Conference Principles of Knowledge Representation and Reasoning (KR12) Rome, Italy. pp 319-328. AAAI Press.

G. De Giacomo, P. Felli, A. Lomuscio.
Synthesizing agent protocols from LTL specifications against multiple partially-observable environments.
Proceedings of the 13th International Conference Principles of Knowledge Representation and Reasoning (KR12), Rome, Italy. pp 457-466. 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
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
Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS12), Valencia, Spain. pp 1107-1114. IFAAMAS Press.

A. Lomuscio, H. Qu, M. Solanki.
Towards verifying contract regulated service composition
Journal of Autonomous Agents and Multi-Agent Systems, Vol 24(3). pp 345-373. 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. LNCS Vol 7084. pp 142-156. Springer.

F. Belardinelli, A.V. Jones, A. Lomuscio.
Model checking temporal-epistemic logic using alternating tree automata
Fundamenta Informaticae, Vol 112(1). pp 19-37. 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, Vol 111(3). pp 339-355. 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.

J. Ezekiel, A. Lomuscio.
A methodology for automatic diagnosability analysis
Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM10). Shanghai, China. LNCS 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. LNCS 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, Vol 106(1). pp 175-190.

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 version of 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. 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, Vol 102(1). pp 77-96. 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.

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. LNCS 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. LNCS 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. LNCS 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.

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. pp 106-121. LNCS Vol 5348. 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.

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. pp 456-461. LNCS Vol 4749. 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. College Publications.

S. Edelkamp, A. Lomuscio (editors).
Proceedings of MoChartIV
4th International Workshop on Model Checking and Artificial Intelligence. LNCS Volume 4428. Springer.

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.

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). pp 29-42. LNCS Vol 4327. Springer.

A. Lomuscio, F. Raimondi, B. Wozna.
Verification of the TESLA protocol with MCMAS-X.
International Workshop on Concurrency, Specification and Programming. Wandlitz, Germany. 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 Vol 4428. Springer.

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. LNCS Vol 4048. Springer.

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. 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, pp 450-454. LNCS Vol 3920. Springer.