Publications

2025

  1. Scalable Neural Network Geometric Robustness Validation via Hölder Optimisation.
    Y. Zhang, P. Kouvaros, A. Lomuscio.
    Proceedings of the 39th Annual Conference on Neural Information Processing Systems (NeurIPS25). San Diego, CA, USA.
  2. Verifiably Robust Contrastive Learning.
    H. Hanspal, A. Lomuscio.
    Proceedings of the 28th European Conference on Artificial Intelligence (ECAI25). Bologna, Italy.
  3. A Scalable Approach to Probabilistic Neuro-symbolic Robustness Verification.
    V. Manginas, N. Manginas, E. Stevinson, S. Varghese, N. Katzouris, G. Paliouras, A. Lomuscio.
    Proceedings of the 19th International Conference on Neurosymbolic Reasoning (NeSY25). Santa Cruz, CA, USA. (Outstanding paper award).
  4. Learning Robust XGBoost Ensembles for Regression Tasks.
    A. Sharma, P. Kouvaros, A. Lomuscio.
    Proceedings of the 41st Conference on Uncertainty in Artificial Intelligence (UAI25). Rio de Janeiro, Brazil.
  5. Improving Weather-based OOD Generalisation in Lidar-based Perception Models via Adversarial Training.
    B. Batten, A. Lomuscio.
    Proceedings of the CVPR2025 Workshop on Workshop on Safe Artificial Intelligence for All Domains (SAID). Nashville, TN, USA.
  6. Robustness to Perturbations in the Frequency Domain: Neural Network Verification and Certified Training.
    H. Hanspal, A. De Palma, A. Lomuscio.
    Proceedings of the IEEE/CVF Winter Workshops of the Conference on Applications of Computer Vision (WACV25). Tucson, AZ, USA. CVF Press.
  7. LTL Verification of Memoryful Neural Agents.
    M. Hosseini, N. Paoletti, A. Lomuscio.
    Proceedings of the 24th International Conference on Autonomous Agents and Multi-agent systems (AAMAS25). Detroit, MI, USA. AAMAS Press.
  8. Dynamic Back-substitution in Bound-propagation-based Neural Network Verification.
    P. Kouvaros, B. Brueckner, P. Henriksen, A. Lomuscio.
    Proceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI-25). Philadelphia, PA, USA. AAAI Press.
  9. Verification of Neural Networks against Convolutional Perturbations via Parameterised Kernels.
    B. Brueckner, A. Lomuscio.
    Proceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI-25). Philadelphia, PA, USA. AAAI Press.

2024

  1. Reducing Return Volatility in Neural Network-Based Asset Allocation via Formal Verification and Certified Training.
    E. Stevinson, A. Lomuscio.
    Proceedings of the 5th ACM International Conference on AI in Finance (ICAIF24). Brooklyn, New York, USA.
  2. Verification of Geometric Robustness of Neural Networks via Piecewise Linear Approximation and Lipschitz Optimisation.
    B. Batten, Y. Zheng, A. De Palma, P. Kouvaros, A. Lomuscio.
    Proceedings of the 27th European Conference on Artificial Intelligence (ECAI24). Santiago de Compostela, Spain.
  3. Expressive Losses for Verified Robustness via Convex Combinations.
    A. De Palma, R. Bunel, K. Dvijotham, M. P. Kumar, R. Stanforth, A. Lomuscio.
    Proceedings of the 12th International Conference on Learning Representations (ICLR24). Vienna, Austria.
  4. Tight Verification of Probabilistic Robustness in Bayesian Neural Networks.
    B. Batten, M. Hosseini, A. Lomuscio.
    Proceedings of the 27th International Conference on Artificial Intelligence and Statistics (AISTATS24). Valencia, Spain.

2023

  1. Verification of Semantic Key Point Detection for Aircraft Pose Estimation.
    P. Kouvaros, F. Leofante, B. Edwards, C. Chung, D. Margineantu, A. Lomuscio.
    Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning (KR23). Rhodes, Greece. AAAI Press.
  2. Verification-friendly Networks: the Case for Parametric ReLUs.
    F. Leofante, P. Henriksen, A. Lomuscio.
    Proceedings of the 36th International Conference on Neural Networks (IJCNN23). Gold Coast, Australia. IEEE Press.
  3. Efficient Verification of Neural Networks against LVM-based Specifications.
    H. Hanspal, A. Lomuscio.
    Proceedings of the 36th IEEE Conference on Computer Vision and Pattern Recognition (CVPR23).
  4. Bounded and Unbounded Verification of RNN-Based Agents in Non-deterministic Environments (extended abstract).
    M. Hosseini, A. Lomuscio.
    Proceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS23). London, UK. IFAAMAS Press.
  5. Towards Robust Contrastive Explanations for Human-Neural Multi-Agent Systems (extended abstract).
    F. Leofante, A. Lomuscio.
    Proceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS23). London, UK. IFAAMAS Press.
  6. A Semidefinite Relaxation based Branch-and-Bound Method for Tight Neural Network Verification.
    J. Lan, B. Brueckner, A. Lomuscio.
    Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA.
  7. Iteratively Enhanced Semidefinite Relaxations for Efficient Neural Network Verification.
    J. Lan, Y. Zheng, A. Lomuscio.
    Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA.
  8. Robust Training of Neural Networks against Bias Field Perturbations.
    P. Henriksen, A. Lomuscio.
    Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA.
  9. A Counter Abstraction Technique for Verifying Properties of Probabilistic Swarm Systems.
    E. Pirovano, A. Lomuscio.
    Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA. Journal Track.

2022

  1. Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications
    F. Belardinelli, A. Lomuscio, V. Malvone, E. Yu.
    Journal of Artificial Intelligence Research.
  2. A Counter Abstraction Technique for Verifying Properties of Probabilistic Swarm Systems
    A. Lomuscio and E. Pirovano.
    Artificial Intelligence. Elsevier.
  3. Repairing Misclassifications in Neural Networks Using Limited Data.
    P. Henriksen, F. Leofante, A. Lomuscio.
    Proceedings of the 37th ACM/SIGAPP Symposium On Applied Computing (SAC22). Virtual Conference.
  4. Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations
    J. Lan, Y. Zheng, A. Lomuscio.
    Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI22). Virtual Conference.
  5. Formal Verification of Neural Agents in Non-deterministic Environments.
    M. Akintunde, E. Botoeva, P. Kouvaros, A. Lomuscio.
    Journal of Autonomous Agents and Multi-Agent Systems, Vol 36(1). Springer.

2021

  1. OSIP: Tightened Bound Propagation for the Verification of ReLU Neural Networks.
    V. Hashemi, P. Kouvaros, A. Lomuscio.
    Proceedings of the 19th International Conference on Software Engineering and Formal Methods (SEFM21). Virtual Conference.
  2. Robustness Learning via Decision Tree Search Robust Optimisation.
    Y-L. Liu, A. Lomuscio.
    Proceedings of the 31st British Machine Vision Conference (BMVC21). Virtual Conference.
  3. Bias Field Robustness Verification of Large Neural Image Classifiers.
    P. Henriksen, K. Hammernik, D. Rueckert, A. Lomuscio.
    Proceedings of the 31st British Machine Vision Conference (BMVC21). Virtual Conference.
  4. Formal Analysis of Neural Network-based Systems in the Aircraft Domain.
    P. Kouvaros, T. Kyono, F. Leofante, A. Lomuscio, D. Margineantu, D. Osipychev, Y. Zheng.
    Proceedings of the 24th International Symposium on Formal Methods (FM21). Virtual conference.
  5. Synthesizing Best-effort Strategies under Multiple Environment Specifications.
    B. Aminof, G. De Giacomo, A. Lomuscio, A. Murano, S. Rubin.
    Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR21). Hanoi, Vietnam. AAAI Press.
  6. Efficient Neural Network Verification via Layer-based Semidefinite Relaxations and Linear Cuts.
    B. Batten, P. Kouvaros, A. Lomuscio, Y. Zheng.
    Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Montreal, Canada.
  7. Reasoning about agents that may know other agents’ strategies.
    F. Belardinelli, S. Knight, A. Lomuscio, B. Maubert, N. Murano, S. Rubin.
    Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Montreal, Canada.
  8. DEEPSPLIT: An Efficient Splitting Method for Neural Network Verification via Indirect Effect Analysis.
    P. Henriksen, A. Lomuscio.
    Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Montreal, Canada.
  9. Towards Scalable Complete Verification of ReLU Neural Networks via Dependency-based Branching.
    P. Kouvaros, A. Lomuscio.
    Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Montreal, Canada.

2020

  1. Verification of multi-agent systems with public actions against strategy logic.
    F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin.
    Artificial Intelligence. Elsevier.
  2. Verifying Fault-Tolerance in Probabilistic Swarm Systems.
    A. Lomuscio, E. Pirovano.
    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.
  3. Synthesizing best-effort strategies under expected and exceptional environment behaviors.
    B. Aminof, G. De Giacomo, A. Lomuscio, A. Murano, S. Rubin.
    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.
  4. MRobust: A Method for Robustness against Adversarial Attacks on Deep Neural Networks.
    Y-L. Liu, A. Lomuscio.
    Proceedings of the 33rd International Conference on Neural Networks (IJCNN20). Edinburgh, UK. IEEE Press.
  5. Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search.
    P. Henriksen, A. Lomuscio.
    Proceedings of the 24th European Conference on Artificial Intelligence (ECAI20). Santiago de Compostela, Spain.
  6. Formal Verification of Neural Agents in Non-Deterministic Environments. (video talk)
    M. Akintunde, E. Botoeva, P. Kouvaros, A. Lomuscio.
    Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Auckland, New Zealand. IFAAMAS Press.
  7. Verifying Strategic Abilities of Neural Multi-agent Systems.
    M. Akintunde, E. Botoeva, P. Kouvaros, A. Lomuscio.
    Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR20). Virtual conference. AAAI Press.
  8. Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems. (video talk)
    A. Lomuscio, E. Pirovano.
    Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Auckland, New Zealand. IFAAMAS Press.
  9. Efficient Verification of Neural Networks via Dependency Analysis.
    E. Botoeva, P. Kouvaros, J. Kronqvist, A. Lomuscio, R. Misener.
    Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20). New York City, New York. AAAI Press.
  10. Model Checking Temporal Epistemic Logic under Bounded Recall.
    F. Belardinelli, A. Lomuscio, E. Yu.
    Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20). New York City, New York. AAAI Press.

2019

  1. An MCTS-based Adversarial Training Method for Image Recognition
    Y-L. Liu, A. Lomuscio.
    Proceedings of the 32nd International Conference on Neural Networks (IJCNN19). Budapest, Hungary. IEEE Press.
  2. Formal Verification of Open Multi-Agent Systems
    P. Kouvaros, A. Lomuscio, E. Pirovano, H. Punchihewa.
    Proceedings of the 18th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS19). Montreal, Canada. IFAAMAS Press.
  3. A Counter Abstraction Technique for the Verification of Probabilistic Swarm Systems
    A. Lomuscio, E. Pirovano.
    Proceedings of the 18th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS19). Montreal, Canada. IFAAMAS Press.
  4. An Abstraction-based Method for Verifying Strategic Properties in Multi-agent Systems with Imperfect Information
    F. Belardinelli, A. Lomuscio, V. Malvone.
    Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI 2019). Honolulu, Hawaii. AAAI Press.
  5. Verification of RNN-Based Neural Agent-Environment Systems
    M. Akintunde, A. Kevorchian, A. Lomuscio, E. Pirovano
    Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI 2019). Honolulu, Hawaii. AAAI Press.

2018

  1. Approximating Perfect Recall when Model Checking Strategic Abilities
    F. Belardinelli, A. Lomuscio, V. Malvone.
    Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR18). Tempe, Arizona. AAAI Press.
  2. Reachability Analysis for Neural Agent-Environment Systems
    M. Akintunde, A. Lomuscio, L. Maganti, E. Pirovano
    Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR18). Tempe, Arizona. AAAI Press.
  3. Symbolic Synthesis of Fault-Tolerance Ratios in Parameterised Multi-Agent Systems
    P. Kouvaros, A. Lomuscio, E. Pirovano.
    Proceedings of the 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI18). Stockholm, Sweden. AAAI Press.
  4. Verifying Emergence of Bounded Time Properties in Probabilistic Swarm Systems
    A. Lomuscio, E. Pirovano.
    Proceedings of the 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI18). Stockholm, Sweden. AAAI Press.
  5. Alternating-time Temporal Logic on Finite Traces
    F. Belardinelli, A. Lomuscio, N. Murano, S. Rubin.
    Proceedings of the 27th International Joint Conference on Artificial Intelligence and 23rd European Conference on Artificial Intelligence (IJCAI-ECAI18). Stockholm, Sweden. AAAI Press.
  6. Introduction to Special Issue on Strategic Reasoning
    A. Lomuscio, M. Y. Vardi (eds).
    Information and Computation. 2018. (Extended versions of selected articles from the 4th International Workshop on Strategic Reasoning, New York, USA, 2016).
  7. Model Checking Multi-Agent Systems against LDLK Specifications on Finite Traces
    J. Kong, A. Lomuscio.
    Proceedings of the 17th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS18). Stockholm, Sweden. IFAAMAS Press.
  8. Decidable Verification of Multi-agent Systems with Bounded Private Actions
    F. Belardinelli, A. Lomuscio, N. Murano. S. Rubin.
    (extended abstract). Proceedings of the 17th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS18). Stockholm, Sweden. IFAAMAS Press.
  9. Towards the Formal Verification of Correctness and Robustness of Robot Swarms (Invited Talk).
    P. Kouvaros, A. Lomuscio.
    Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic.

2017

  1. An approach to reachability analysis for feed-forward ReLU neural Networks
    A. Lomuscio, L. Maganti.
    arXiv preprint. arXiv:1706.07351 [cs.AI].
  2. Practical Verification of Multi-Agent Systems against SLK Specifications
    P. Cermak, A. Lomuscio, F. Mogavero, A. Murano.
    Information and Computation.
  3. Verifying Fault-tolerance in Parameterised Multi-Agent Systems
    P. Kouvaros, A. Lomuscio.
    Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 288-294. AAAI Press.
  4. Model Checking Multi-Agent Systems against LDLK Specifications
    J. Kong, A. Lomuscio.
    Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 1138-1144. AAAI Press.
  5. Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic
    F. Belardinelli, A. Lomuscio, N. Murano. S. Rubin.
    Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 91-97. AAAI Press.
  6. Parameterised Verification of Data-aware Multi-agent Systems.
    F. Belardinelli, P. Kouvaros, A. Lomuscio.
    Proceedings of the 26th Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. pp 98-104. AAAI Press.
  7. Compositional Neural-Network Modeling of Complex Analog Circuits.
    R. Hasani, D Haerle, C. Baumgartner, A. Lomuscio, R Grosu.
    Proceedings of the 30th International Conference on Neural Networks (IJCNN17). Anchorage, USA. pp 2235-2242. IEEE Press.
  8. Symbolic Model Checking Multi-Agent Systems against CTL*K Specifications
    J. Kong, A. Lomuscio.
    Proceedings of the 16th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS17). Sao Paolo, Brazil. pp 114-122. IFAAMAS Press.
  9. Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect Information
    F. Belardinelli, A. Lomuscio.
    Proceedings of the 16th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS17). Sao Paolo, Brazil. pp 1259-1267. IFAAMAS Press.
  10. Verification of Multi-agent Systems with Imperfect Information and Public Actions
    F. Belardinelli, A. Lomuscio, N. Murano. S. Rubin.
    Proceedings of the 16th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS17). Sao Paolo, Brazil. pp 1268-1276. IFAAMAS Press.
  11. Parameterised Verification of Infinite State Multi-Agent Systems via Predicate Abstraction
    P. Kouvaros, A. Lomuscio.
    Proceedings of the 31th AAAI Conference on Artificial Intelligence (AAAI17). San Francisco (CA), USA. pp 3013-3020. AAAI Press.
  12. MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems
    A. Lomuscio, H. Qu, F. Raimondi
    International Journal on Software Tools for Technology Transfer. Vol 19(1); pp 9–30. Springer. 2017.

2016

  1. A Three-value Abstraction Technique for the Verification of Epistemic Properties in Multi-agent Systems
    F. Belardinelli, A. Lomuscio.
    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.
  2. Proceedings of the 4th International Workshop on Strategic Reasoning (SR2016)
    A. Lomuscio, M. Y. Vardi, eds.
    New York, USA.
  3. Parameterised Model Checking for Alternating-time Temporal Logic
    P. Kouvaros, A. Lomuscio.
    Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands.
  4. Abstraction-based Verification of Infinite-state Reactive Modules
    F. Belardinelli, A. Lomuscio.
    Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands.
  5. Agent-based Refinement for Predicate Abstraction of Multi-Agent Systems.
    F. Belardinelli, A. Lomuscio, J. Michaliszyn.
    Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands.
  6. Formal Verification of Opinion Formation in Swarms
    P. Kouvaros, A. Lomuscio.
    Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. IFAAMAS Press.
  7. Verifying Security Properties in Unbounded Multiagent Systems
    I. Boureanu, P. Kouvaros, A. Lomuscio.
    Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. IFAAMAS Press.
  8. Verification of Multi-Agent Systems via Predicate Abstraction against ATLK specifications
    A. Lomuscio, J. Michaliszyn.
    Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. IFAAMAS Press.
  9. Model Checking Multi-Agent Systems against Epistemic HS Specifications with Regular Expressions
    A. Lomuscio, J. Michaliszyn.
    Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR16). Cape Town, South Africa. AAAI Press.
  10. Parameterised Verification for Multi-Agent Systems
    P. Kouvaros, A. Lomuscio.
    Artificial Intelligence. Elsevier.

2015

  1. Verification of GSM-based Artifact-centric Systems by Predicate Abstraction
    P. Gonzalez, A. Griesmayer, A. Lomuscio.
    Proceedings of the 13th International Conference on Service Oriented Computing (ICSOC15). Goa, India.
  2. Verifying Emergent Properties of Swarms
    P. Kouvaros, A. Lomuscio.
    Proceedings of the Twenty-Fourth International Conference on Artificial Intelligence (IJCAI15). Buonos Aires, Argentina. AAAI Press.
  3. Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems
    F. Belardinelli, D. Grossi, A. Lomuscio.
    Proceedings of the Twenty-Fourth International Conference on Artificial Intelligence (IJCAI15). Buonos Aires, Argentina. AAAI Press.
  4. MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems
    A. Lomuscio, H. Qu, F. Raimondi
    International Journal on Software Tools for Technology Transfer.
  5. Handbook of Epistemic Logic
    A. Lomuscio, W. Penczek. Model Checking Temporal Epistemic Logic. Chapter 8 of the
    H. van Ditmarsch, J. Halpern, W. van der Hoek, and B. Kooi (eds.). College Publications, pp 397-441.
  6. Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions.
    A. Lomuscio, J. Michaliszyn.
    Proceedings of the 14th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS15). Istanbul, Turkey. IFAAMAS Press.
  7. Verification of Multi-Agent Systems via SDD-based Model Checking (Extended Abstract)
    A. Lomuscio, H. Paquet.
    Proceedings of the 14th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS15). Istanbul, Turkey. IFAAMAS Press.
  8. A Counter Abstraction Technique for the Verification of Robot Swarms
    P. Kouvaros, A. Lomuscio.
    Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI15). Austin, Texas. pp 2081-2088. AAAI Press.
  9. Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications
    P. Cermak, A. Lomuscio, A. Murano.
    Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI15). Austin, Texas. pp 2038-2044. AAAI Press.

2014

  1. Verification of Agent-based Artifact Systems
    F. Belardinelli, A. Lomuscio, F. Patrizi.
    Journal of Artificial Intelligence Research. Vol 51, pp 333–376. AAAI Press.
  2. Decidability of model checking multi-agent systems against some EHS specifications
    A. Lomuscio, J. Michaliszyn.
    Proceedings of the 21st European Conference on Artificial Intelligence (ECAI14). Prague, Czech Republic, pp 543-548. IOS Press.
  3. Proceedings of the 13th International Conference on Autonomous Agents and Multiagent Systems
    A. Lomuscio, P. Scerri, A. Bazzan, M. Huhns (Eds.).
    (AAMAS14). IFAAMAS Press.
  4. Proceedings of the Satellite Events of the 11th International Conference on Service Oriented Computing
    A. Lomuscio, S. Nepal, F. Patrizi, B. Benatallah, I. Brandic (Eds.).
    (ICSOC14). LNCS Vol 8377. Springer.
  5. MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
    P. Cermak, A. Lomuscio, F. Mogavero, A. Murano.
    Proceedings of the 26th International Conference on Computer Aided Verification (CAV14). Vienna, Austria. pp 525-532. Springer
  6. Model Checking Unbounded Artifact-Centric Systems
    A. Lomuscio, J. Michaliszyn.
    Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR14), Vienna, Austria. pp 488-497. AAAI Press.
  7. An abstraction technique for the verification of multi-agent systems against ATL specifications
    A. Lomuscio, J. Michaliszyn.
    Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR14), Vienna, Austria. pp 428-437. AAAI Press.

2013

  1. Model checking GSM-based Multi-Agent systems
    P. Gonzalez, A. Griesmayer, A. Lomuscio.
    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.
  2. An Epistemic Halpern-Shoham Logic
    A. Lomuscio, J. Michaliszyn.
    Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13). Beijing, China. pp 1010-1016. AAAI Press.
  3. Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems
    F. Belardinelli, A. Lomuscio.
    Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13). Beijing, China. pp 725-731. AAAI Press.
  4. A Cutoff Technique for the Verification of Parameterised Interpreted Systems with Parameterised Environments
    P. Kouvaros, A. Lomuscio.
    Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13). pp 2013-2019. AAAI Press.
  5. Model Checking Distributed Systems against Temporal-Epistemic Specifications
    A. Griesmayer, A. Lomuscio.
    Proceedings of the IFIP Joint International Conference on Formal Techniques for Distributed Systems (FORTE/FMOODS). Florence, Italy. LNCS Vol 7892. pp 130-145. Springer.
  6. Automatic Verification of Parametrised Interleaved Multi-Agent Systems
    P. Kouvaros, A. Lomuscio.
    Proceedings of the 12th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS13). Saint Paul, MN, USA. pp 861-868. IFAAMAS Press.
  7. Assume-Guarantee Reasoning with Local Specifications
    A. Lomuscio, B. Strulo, N. Walker, P. Wu.
    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.

2012

  1. Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results
    F. Belardinelli, A. Lomuscio.
    Journal of Artificial Intelligence Research, Vol 45. pp 1-45.
  2. Verification of GSM-based artifact-centric systems through finite abstraction
    F. Belardinelli, A. Lomuscio, F. Patrizi.
    Proceedings of the 10th International Conference on Service Oriented Computing (ISCOC12). Shanghai, China. Lecture Notes in Computer Science, Vol 7636. pp 17-31. Springer.
  3. A Framework for Automated and Certified Refinement Steps (arXiv pre-print)
    A. Griesmayer, Z. Liu, C. Morisset, S. Wang
    accepted for publication in the Journal on Innovations in Systems and Software Engineering, 2012, Springer.
  4. Verifying GSM-based Business Artifacts
    P. Gonzalez, A. Griesmayer, A. Lomuscio.
    Proceedings of the 2012 IEEE International Conference on Web Services (ICWS2012). Honolulu, USA. pp 25-32. IEEE Press.
  5. Exploiting Model Variability in ABS to Verify Distributed Algorithms
    W. Leister, J. Bjørk, R. Schlatte, E. B. Johnsen, A. Griesmayer.
    International Journal on Advances in Telecommunication Vol 5(1&2). pp 55-68. ARIA Journals.
  6. An Abstraction Technique for the Verification of Artifact-Centric Systems
    F. Belardinelli, A. Lomuscio, F. Patrizi.
    Proceedings of the 13th International Conference Principles of Knowledge Representation and Reasoning (KR12) Rome, Italy. pp 319-328. AAAI Press.
  7. Synthesizing agent protocols from LTL specifications against multiple partially-observable environments.
    G. De Giacomo, P. Felli, A. Lomuscio.
    Proceedings of the 13th International Conference Principles of Knowledge Representation and Reasoning (KR12), Rome, Italy. pp 457-466. AAAI Press.
  8. Automated Verification of Quantum Protocols using MCMAS
    F. Belardinelli, P. Gonzalez, A. Lomuscio.
    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.
  9. Automatic Verification of Epistemic Specifications under Convergent Equational Theories
    I. Boureanu, A.V. Jones, A. Lomuscio.
    Proceedings of the 11th International Conferenceon Autonomous Agents and Multi-Agent systems (AAMAS12) Valencia, Spain. IFAAMAS Press.
  10. Group Synthesis for Parametric Temporal-Epistemic Logic
    A.V. Jones, M. Knapik, A. Lomuscio, W. Penczek.
    Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS12), Valencia, Spain. pp 1107-1114. IFAAMAS Press.

2011

  1. Towards verifying contract regulated service composition
    A. Lomuscio, H. Qu, M. Solanki.
    Journal of Autonomous Agents and Multi-Agent Systems, Vol 24(3). pp 345-373. Springer.
  2. Verification of Deployed Artifact Systems via Data Abstraction
    F. Belardinelli, A. Lomuscio, F. Patrizi.
    Proceedings of the 9th International Conference on Service Oriented Computing (ICSOC11). Paphos, Cyprus. LNCS Vol 7084. pp 142-156. Springer.
  3. Model checking temporal-epistemic logic using alternating tree automata
    F. Belardinelli, A.V. Jones, A. Lomuscio.
    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.
  4. A computationally grounded semantics for artifact centric systems and abstraction results
    F. Belardinelli, A. Lomuscio, F. Patrizi.
    Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI11). Barcelona, Spain. pp 738-743. AAAI Press.
  5. Verifying fault tolerance and self-diagnosability of an autonomous underwatervehicle
    J. Ezekiel, A. Lomuscio, L. Molnar,S. Veres.
    Poster Presentation. Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI11). Barcelona, Spain. pp 1659-1664. AAAI Press.
  6. Runtime monitoring of contract regulated web services
    A. Lomuscio, W. Penczek, M. Solanki, M. Szreter.
    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.

2010

  1. A methodology for automatic diagnosability analysis
    J. Ezekiel, A. Lomuscio.
    Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM10). Shanghai, China. LNCS Vol 6447. pp 549-564. Springer.
  2. Assume-Guarantee Reasoning with Local Specifications
    A. Lomuscio, B. Strulo, N. Walker, P. Wu.
    Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM10). Shanghai, China. LNCS Vol 6447. pp 204-219. Springer.
  3. First-Order Linear-time Epistemic Logic Group Knowledge: An Axiomatisation of the Monodic Fragment
    F. Belardinelli, A. Lomuscio.
    Fundamenta Informaticae, Vol 106(1). pp 175-190.
  4. Partial order reduction for model checking interleaved multi-agent systems
    A. Lomuscio, W. Penczek, H. Qu.
    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.
  5. Distributed BDD-based BMC for the Verification of Multi-Agent Systems
    A. V. Jones, A. Lomuscio.
    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.
  6. Non-elementary speedup for model checking synchronous perfect recall
    M. Cohen, A. Lomuscio.
    Short paper. Proceedings of the 19th European Conference on Artificial Intelligence (ECAI10). Lisbon, Portugal. pp 1077-1078. IOS Press.
  7. Parallel Model Checking for Temporal Epistemic Logic
    M. Kwiatkowska, A. Lomuscio, H. Qu.
    Proceedings of the 19th European Conference on Artificial Intelligence (ECAI10). Lisbon, Portugal. pp 543-548. IOS Press.
  8. Automatic data abstraction in model checking Multi-Agent Systems
    A. Lomuscio, H. Qu, F. Russo.
    Proceedings of the 6th International Workshop on Model Checking and Artificial Intelligence (MochartVI). Atlanta, USA. pp 61-76.
  9. Interactions between knowledge and time in a first-order logic for multi-agent systems
    F. Belardinelli, A. Lomuscio.
    Proceedings of the 12th International Conference on Knowledge Representation and Reasoning (KR10). Toronto, Canada. pp 38-48. AAAI Press.
  10. Model checking optimisation-based congestion control models
    A. Lomuscio, B. Strulo, N. Walker, P. Wu.
    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.
  11. Model checking detectability of attacks in multiagent systems
    I. Boureanu, M. Cohen, A. Lomuscio.
    Proceedings of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS10). Toronto, Canada. pp 691-698. IFAAMAS Press.

2009

  1. A compilation method for the verification of temporal-epistemic properties of cryptographic protocols
    I. Boureanu, M. Cohen, A. Lomuscio.
    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.
  2. An automated approach to verifying diagnosability in multi-agent systems.
    J. Ezekiel, A. Lomuscio.
    Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM09). Hanoi, Vietnam. pp 51-60. IEEE Press.
  3. A data symmetry reduction technique for temporal-epistemic logic
    M. Cohen, M. Dam, A. Lomuscio, H. Qu.
    Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA09). Macao, SAR. China. LNCS Vol 5799. pp 69-83. Springer.
  4. A Symmetry Reduction technique for model checking temporal epistemic logic
    M. Cohen, M. Dam, A. Lomuscio, H.Qu
    Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI09). Pasadena, USA. pp 721-726. AAAI Press.
  5. First-Order Linear-time Epistemic Logic Group Knowledge: An Axiomatisation of the Monodic Fragment
    F. Belardinelli, A. Lomuscio.
    Proceedings of the 16th Workshop on Logic, Language, Information and Computation. Tokyo, Japan. LNCS Vol 5514. pp 140-154. Springer.
  6. MCMAS: A model checker for the verification of multi-agent systems
    A. Lomuscio, H. Qu, F. Raimondi
    Proceedings of the 21th International Conference on Computer Aided Verification (CAV 2009). Grenoble, France. LNCS Vol 5643. pp 682-688. Springer.
  7. Quantified Epistemic Logic for reasoning about knowledge in Multi-Agent Systems
    F. Belardinelli, A. Lomuscio.
    Artificial Intelligence, Vol 173(9-10). pp 982-1013. Elsevier.
  8. Mapping OWL-S processes to multi agent systems: A verification oriented approach
    A. Lomuscio, M. Solanki.
    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).
  9. Combining fault injection and model checking to verify fault tolerance in multi-agent systems.
    J. Ezekiel, A. Lomuscio.
    Proceedings of the 8th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS09). Budapest, Hungary. pp 113-120. IFAAMAS Press.
  10. Abstraction in model checking multi-agent systems
    M. Cohen, M. Dam, A. Lomuscio, F. Russo
    Proceedings of the 8th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS09). Budapest, Hungary. pp 945-952. IFAAMAS Press.

2008

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

2007

  1. Bounded model checking knowledge and real time
    A. Lomuscio, W. Penczek, B. Wozna.
    Artificial Intelligence. Vol 171(16-17). pp 1011-1038. Elsevier.
  2. Symbolic model checking for temporal epistemic logic
    A. Lomuscio, W. Penczek.
    SIGACT News Logic Column. ACM SIGACT News. Logic Column. 38(3), pp 76-100. 2007. ACM Press.
  3. Model checking security protocols: a multiagent systems approach
    A. Lomuscio, W. Penczek.
    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.
  4. Verifying Temporal Epistemic properties of Web service compositions
    A. Lomuscio, H. Qu, M. Sergot, M. Solanki.
    Proceedings of the 5th International Conference on Service Oriented Computing (ICSOC07). Vienna, Austria. pp 456-461. LNCS Vol 4749. Springer.
  5. A complete quantified epistemic logic for reasoning about message passing systems
    F. Belardinelli, A. Lomuscio.
    Proceedings of the 8th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA VIII). Porto, Portugal.
  6. Quantified epistemic logics with flexible terms
    F. Belardinelli, A. Lomuscio.
    A Meeting of the Minds: Proceedings of the Workshop on Logic, Rationality and Interaction. Beijing, China. College Publications.
  7. Proceedings of MoChartIV
    S. Edelkamp, A. Lomuscio (editors).
    4th International Workshop on Model Checking and Artificial Intelligence. LNCS Volume 4428. Springer.
  8. Verification of the Tesla protocol in MCMAS-X
    A. Lomuscio, F. Raimondi, B. Wozna.
    Fundamenta Informaticae, vol 79 (3-4). pp 473-486. IOS Press.
  9. A temporal epistemic logic with a reset operation
    A. Lomuscio, B. Wozna.
    Proceedings of the 6th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS07). Honolulu, USA. IFAAMAS Press.
  10. A quantified epistemic logic for reasoning about multi-agent systems
    F. Belardinelli, A. Lomuscio.
    Proceedings of the 6th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS07). Short paper. Honolulu, USA. IFAAMAS Press.
  11. Verification of knowledge and time with NuSMV
    A. Lomuscio, C. Pecheur, F. Raimondi.
    Proceedings of the 20th International Conference on Artificial Intelligence (IJCAI07), Hyderabadad, India.

2006

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