End-to-End Verification of Neuro-symbolic Automata via Contrastive Logit-Gaps
Forthcoming, NeurIPS 2026
Publications
237 publications, grouped by year.
237 publications
2026
Validating, Not Sampling: Region-Level Robustness of Vision-Language and Vision-Language-Action Models
arXiv:2609.22293 (2026). Preprint.
Eliciting Intrinsic Hallucinations in LLMs via Semantically Equivalent Adversarial Attacks
Proceedings of the 3rd International Conference on Language Modeling (COLM26). San Francisco, CA, USA.
IoUCert: Robustness Verification for anchor-based Object Detectors
Proceedings of the 19th European Conference on Computer Vision (ECCV26). Malmoe, Sweden. Springer.
Hybrid Robustness Verification for Spatio-temporal Neural Networks
Proceedings of the 9th International Symposium on AI Verification (SAIV26). Lisbon, Portugal.
A Robust Out-of-Distribution Detection Framework via Synergistic Smoothing
Proceedings of the 39th IEEE Conference on Computer Vision and Pattern Recognition (CVPR26). Denver, CO, USA. Computer Vision Foundation / IEEE.
Lipschitz Optimization for Formal Verification of Homographies
Proceedings of the 39th IEEE Conference on Computer Vision and Pattern Recognition (CVPR26). Denver, CO, USA. Computer Vision Foundation / IEEE.
Out-of-Distribution Detection using Counterfactual Distance
Proceedings of the IJCAI26 Workshop on Explainable AI. Bremen, Germany.
Safe and Scalable Multi-agent Coordination with Reconstructed Level-k Monte Carlo Tree Search
Proceedings of the 25th International Conference on Autonomous Agents and Multi-agent Systems (AAMAS26). Paphos, Cyprus. IFAAMAS Press.
Certified Background-Invariant Training via Latent Generative Models
Proceedings of the AAAI26 Workshop on Artificial Intelligence for Air Transportation (AI4AT). Singapore.
Improving Neural Network Robustness to Convolutional Perturbations Through Certified Training
Proceedings of the AAAI26 Workshop on Artificial Intelligence for Cyber Security (AICS). Singapore.
2025
Scalable Neural Network Geometric Robustness Validation via Hölder Optimisation
Proceedings of the 39th Annual Conference on Neural Information Processing Systems (NeurIPS25). San Diego, CA, USA.
Verifiably Robust Contrastive Learning
Proceedings of the 28th European Conference on Artificial Intelligence (ECAI25). Bologna, Italy.
A Scalable Approach to Probabilistic Neuro-symbolic Robustness Verification
Proceedings of the 19th International Conference on Neurosymbolic Reasoning (NeSY25). Santa Cruz, CA, USA. (Outstanding paper award).
Learning Robust XGBoost Ensembles for Regression Tasks
Proceedings of the 41st Conference on Uncertainty in Artificial Intelligence (UAI25). Rio de Janeiro, Brazil.
Improving Weather-based OOD Generalisation in Lidar-based Perception Models via Adversarial Training
Proceedings of the CVPR2025 Workshop on Safe Artificial Intelligence for All Domains (SAID). Nashville, TN, USA.
Robustness to Perturbations in the Frequency Domain: Neural Network Verification and Certified Training
Proceedings of the IEEE/CVF Winter Workshops of the Conference on Applications of Computer Vision (WACV25). Tucson, AZ, USA. CVF Press.
LTL Verification of Memoryful Neural Agents
Proceedings of the 24th International Conference on Autonomous Agents and Multi-agent Systems (AAMAS25). Detroit, MI, USA. IFAAMAS Press.
Dynamic Back-substitution in Bound-propagation-based Neural Network Verification
Proceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI25). Philadelphia, PA, USA. AAAI Press.
Verification of Neural Networks against Convolutional Perturbations via Parameterised Kernels
Proceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI25). Philadelphia, PA, USA. AAAI Press.
2024
Reducing Return Volatility in Neural Network-Based Asset Allocation via Formal Verification and Certified Training
Proceedings of the 5th ACM International Conference on AI in Finance (ICAIF24). Brooklyn, New York, NY, USA.
Verification of Geometric Robustness of Neural Networks via Piecewise Linear Approximation and Lipschitz Optimisation
Proceedings of the 27th European Conference on Artificial Intelligence (ECAI24). Santiago de Compostela, Spain.
Expressive Losses for Verified Robustness via Convex Combinations
Proceedings of the 12th International Conference on Learning Representations (ICLR24). Vienna, Austria.
Tight Verification of Probabilistic Robustness in Bayesian Neural Networks
Proceedings of the 27th International Conference on Artificial Intelligence and Statistic (AISTATS24). Valencia, Spain. PMLR.
2023
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.
Verification-friendly Networks: the Case for Parametric ReLUs
Proceedings of the 36th International Conference on Neural Networks (IJCNN23). Gold Coast, Australia. IEEE Press.
Efficient Verification of Neural Networks against LVM-based Specifications
Proceedings of the 36th IEEE Conference on Computer Vision and Pattern Recognition (CVPR23). Montreal, Canada. Computer Vision Foundation / IEEE.
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.
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.
Robust Training of Neural Networks against Bias Field Perturbations
Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA.
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.
Iteratively Enhanced Semidefinite Relaxations for Efficient Neural Network Verification
Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). Washington, DC, USA.
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.
2022
Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications
Journal of Artificial Intelligence Research. Vol.73.
A Counter Abstraction Technique for Verifying Properties of Probabilistic Swarm Systems
Artificial Intelligence. Elsevier. Vol 305.
Repairing Misclassifications in Neural Networks Using Limited Data
Proceedings of the 37th ACM/SIGAPP Symposium On Applied Computing (SAC22), pp 1031-1038. ACM. Virtual Conference.
Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations
Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI22). Virtual Conference.
Formal Verification of Neural Agents in Non-deterministic Environments
Journal of Autonomous Agents and Multi-Agent Systems, Vol 36(1). Springer.
2021
Robustness Learning via Decision Tree Search Robust Optimisation
Proceedings of the 31st British Machine Vision Conference (BMVC21). Virtual Conference.
Bias Field Robustness Verification of Large Neural Image Classifiers
Proceedings of the 31st British Machine Vision Conference (BMVC21).
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.
Formal Analysis of Neural Network-based Systems in the Aircraft Domain
Proceedings of the 24th International Symposium on Formal Methods (FM21). Virtual conference.
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.
DEEPSPLIT: An Efficient Splitting Method for Neural Network Verification via Indirect Effect Analysis
Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Virtual conference. Ijcai.org.
Towards Scalable Complete Verification of ReLU Neural Networks via Dependency-based Branching
Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Virtual conference. Ijcai.org.
Efficient Neural Network Verification via Layer-based Semidefinite Relaxations and Linear Cuts
Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Virtual conference. Ijcai.org.
Reasoning about agents that may know other agents’ strategies
Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Virtual conference. Ijcai.org.
Proceedings of the 20th International Conference on Autonomous Agents and Multiagent Systems (AAMAS21)
Virtual conference. IFAAMAS Press.
Verification of Multi-Agent Systems with Public Actions against Strategy Logic
Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21). Journal Track. Virtual Conference. Ijcai.org
2020
Verifying Strategic Abilities of Neural-symbolic Multi-agent Systems
Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR20). Rhodes, Greece. IJCAI Press.
Verification of Multi-Agent Systems with Public Actions against Strategy Logic
Artificial Intelligence. Vol 285, pp 103302, Elsevier.
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.
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.
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.
Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search
Proceedings of the 24th European Conference on Artificial Intelligence (ECAI20). Santiago de Compostela, Spain.
Formal Verification of Neural Agents in non-Deterministic Environments
Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Auckland, New Zealand. IFAAMAS Press.
Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems
Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS20). Auckland, New Zealand. IFAAMAS Press.
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.
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.
2019
Imperfect Information in Alternating- time Temporal Logic on Finite Traces
Proceedings of the 22nd International Conference on Principles and Practice of Multi-Agent Systems (PRIMA19). Turin, Italy. Springer.
An MCTS-based Adversarial Training Method for Image Recognition
Proceedings of the 32nd International Conference on Neural Networks (IJCNN19). Budapest, Hungary. IEEE Press.
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 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.
Verification of RNN-Based Neural Agent-Environment Systems
Proceedings of the 33th AAAI Conference on Artificial Intelligence (AAAI19). Honolulu, HI, USA. AAAI Press.
An Abstraction-based Method for Verifying Strategic Properties in Multi-agent Systems with Imperfect Information
Proceedings of the 33th AAAI Conference on Artificial Intelligence (AAAI19). Honolulu, HI, USA. AAAI Press.
2018
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.
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.
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.
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.
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.
Introduction to Special Issue on Strategic Reasoning
Information and Computation. Vol 261, Part 4. 2018. (Extended and selected articles from the 4th International Workshop on Strategic Reasoning, New York, USA, 2016).
Information and Computation · 4th International Workshop on Strategic Reasoning
Introduction to Special Issue on Temporal Representation and Reasoningg
Information and Computation. Vol 259, Part 3. 2018. (Extended selected articles from the 22nd International Symposium on Temporal Representation and Reasoning (TIME2015), Germany, 2015).
22nd International Symposium on Temporal Representation and Reasoning (TIME2015)
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.
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.
Practical Verification of Multi-Agent Systems against SLK Specifications
Information and Computation, vol. 261, part 3, pp. 588–614 (2018).
2017
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 (ICTCS17/CILC17). CEUR-WS.org.
An approach to reachability analysis for feed-forward ReLU neural Networks
arXiv preprint. arXiv:1706.07351 [cs.AI].
Verifying Fault-tolerance in Parameterised Multi-Agent Systems
Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 288-294. AAAI Press.
Model Checking Multi-Agent Systems against LDLK Specifications
Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 1138-1144. AAAI Press.
Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic
Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. 91-97. AAAI Press.
Parameterised Verification of Data-aware Multi-agent Systems
Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI17). Melbourne, Australia. pp 98-104. AAAI Press.
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.
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.
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.
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.
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.
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.
Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems
Information and Computation 254(2), 167–194 (2017).
2016
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.
Proceedings of the 4th International Workshop on Strategic Reasoning (SR2016)
New York (NY), USA.
Parameterised Model Checking for Alternating-time Temporal Logic
Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands. pp 1230-1238. IOS Press.
Abstraction-based Verification of Infinite-state Reactive Modules
Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands. 725-733. IOS Press.
Agent-based Refinement for Predicate Abstraction of Multi-Agent Systems
Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI16). The Hague, the Netherlands. pp 286-294. IOS Press.
Formal Verification of Opinion Formation in Swarms
Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. pp 1200-1209. IFAAMAS Press.
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. Singapore. pp 662-670. IFAAMAS Press.
Verifying Security Properties in Unbounded Multiagent Systems
Proceedings of the 15th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS16). Singapore. pp 1209-1218. IFAAMAS Press.
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. pp 298-308. AAAI Press.
Parameterised Verification for Multi-Agent Systems
Artificial Intelligence. Elsevier.
2015
Verification of GSM-based Artifact-centric Systems by Predicate Abstraction
Proceedings of the 13th International Conference on Service Oriented Computing (ICSOC15). Goa, India. Lecture Notes in Computer Science. Vol 9435, pp 253-268. Springer.
Verifying Emergent Properties of Swarms
Proceedings of the 24th Conference on Artificial Intelligence (IJCAI15). Buenos Aires, Argentina. pp 1083-1089. AAAI Press.
Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems
Proceedings of the 24th International Conference on Artificial Intelligence (IJCAI15). Buenos Aires, Argentina. pp 854-860. AAAI Press.
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.). pp 397-441. College Publications.
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. pp 189-198. IFAAMAS Press.
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. pp 1713-1714. IFAAMAS Press.
A Counter Abstraction Technique for the Verification of Robot Swarms
Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI15). Austin (TX), USA. pp 2081-2088. AAAI Press.
Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications
Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI15). Austin, Texas. pp 2038-2044. AAAI Press.
2014
Verification of Agent-based Artifact Systems
Journal of Artificial Intelligence Research. Vol 51, pp 333--376. AAAI Press.
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.
Proceedings of the 13th International Conference on Autonomous Agents and Multiagent Systems
(AAMAS14). IFAAMAS Press.
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. Lecture Notes in Computer Science. Vol 8377, pp 525-532. Springer.
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.
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.
Post-Proceedings of the Satellite Events of the 11th International Conference on Service Oriented Computing
(ICSOC13). Lecture Notes in Computer Science, Vol 8377. Springer.
2013
Model checking GSM-based Multi-Agent systems
Proceedings of the Satellite Events of the 11th International Conference on Service Oriented Computing. Lecture Notes in Computer Science, 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.)
An Epistemic Halpern-Shoham Logic
Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13). Beijing, China. pp 1010-1016. AAAI Press.
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.
A Cutoff Technique for the Verification of Parameterised Interpreted Systems with Parameterised Environments
Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI13). Beijing, China. pp 2013-2019. AAAI Press.
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. Vol 7892, pp 130-145. Lecture notes in Computer Science. Springer.
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.
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. Lecture Notes in Computer Science. Vol 6447, pp 204-219. Springer.
2012
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.
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.
Verifying GSM-based Business Artifacts
Proceedings of the 19th International Conference on Web Services (ICWS12). Honolulu, USA. pp 25-32. IEEE Press.
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.
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.
Symbolic Model Checking for temporal-epistemic logics
Logic Programs, Norms and Action - Essays in Honor of Marek J. Sergot on the Occasion of His 60th Birthday. Lecture Notes in Computer Science. Vol 7360, pp 172-195. Springer. 2012. A previous version of this paper appeared in SIGACT News Logic Column. ACM SIGACT News. Logic Column. 38(3), pp 76-100. 2007. ACM Press.
The Scientific Contribution of Marek Sergot
Logic Programs, Norms and Action - Essays in Honor of Marek J. Sergot on the Occasion of His 60th Birthday. Lecture Notes in Computer Science. Vol 7360, pp 4-11. Springer. 2012.
Automated Verification of Quantum Protocols using MCMAS
Proceedings of 10th Workshop on Quantitative Aspects of Programming Languages (QAPL12). Tallin, Estonia. Electronic Proceedings in Theoretical Computer Science. Vol 85, pp 48-62.
Automatic Verification of Epistemic Specifications under Convergent Equational Theories
Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS12). Valencia, Spain. pp 1141-1148. IFAAMAS Press.
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. Best paper nomination.
2011
Towards verifying contract regulated service composition
Journal of Autonomous Agents and Multi-Agent Systems. pp 345-373, Vol 24(3), Springer.
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.
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.
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.
Verifying fault tolerance and self-diagnosability of an autonomous underwater vehicle
Poster Presentation. Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI11). Barcelona, Spain. pp 1659-1664. AAAI Press.
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
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.
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.
First-Order Linear-time Epistemic Logic Group Knowledge: An Axiomatisation of the Monodic Fragment
Fundamenta Informaticae. pp 175-190, Vol 106(1).
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.
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.
Parallel Model Checking for Temporal Epistemic Logic
Proceedings of the 19th European Conference on Artificial Intelligence (ECAI10). Lisbon, Portugal. pp 543-548. IOS Press.
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.
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.
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.
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
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.
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.
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.
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.
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.
MCMAS: A model checker for the verification of multi-agent systems
Proceedings of the 21th International Conference on Computer Aided Verification (CAV09). Grenoble, France. Lecture Notes in Computer Science. Vol 5643 pp 682-688. Springer.
Quantified Epistemic Logic for reasoning about knowledge in Multi-Agent Systems
Artificial Intelligence. Vol 173(9-10), pp 982-1013. Elsevier.
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)).
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.
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
Towards verifying contract regulated service composition
Proceedings of the 8th International Conference on Web Services (ICWS08). Beijing, China. pp 255-261. IEEE Press.
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 Science. Vol 5348, pp 106-121. Springer.
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.
LDYIS: A framework for model checking security protocols
Fundamenta Informaticae, vol 85 (1-4), pp 359-375. IOS Press.
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
Bounded model checking knowledge and real time
Artificial Intelligence. Vol 171(16-17), pp 1011-1038. Elsevier.
Symbolic model checking for temporal epistemic logic
SIGACT News Logic Column. ACM SIGACT News. Logic Column. 38(3), pp 76-100. 2007. ACM Press.
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.
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.
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.
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.
Proceedings of MoChartIV
4th International Workshop on Model Checking and Artificial Intelligence. Springer LNCS Volume 4428.
Verification of the Tesla protocol in MCMAS-X
Fundamenta Informaticae, vol 79 (3-4), pp 473-486. IOS Press.
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.
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.
Verification of knowledge and time with NuSMV
Proceedings of the 20th International Conference on Artificial Intelligence (IJCAI07), Hyderabadad, India.
Automatic Verification of Multi-Agent Systems by Model Checking via Ordered Binary Decision Diagrams
Journal of Applied Logic 5(2), 235–251 (2007).
2006
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.
Verification of the TESLA protocol with MCMAS-X
Proceedings of CS&P, International Workshop on Concurrency, Specification and Programming. Wandlitz, Germany. Humboldt University.
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 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.
Proceedings of LCMAS3
Workshop on Logic and Communication in Multi-Agent Systems. Electronic lecture notes in Theoretical Computer Science. Volume 157:4. Elsevier.
Comparing BDD and SAT based techniques for model checking Chaum's Dining cryptography protocol
Fundamenta Informaticae. Vol 72. pp 215--234. IOS Press.
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.
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.
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 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.
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.
2005
A combination of explicit and deductive knowledge with branching time: completeness and decidability results
Post-proceedings of DALT'05, third workshop on Declarative Agent Languages and Technologies, Springer Verlag, LNCS Volume 3904 (a previous version of this paper was presented at CS&P, International Workshop on Concurrency, Specification and Programming. Ruciane, Poland).
Applications of model checking for multi-agent systems: verification of diagnosability and recoverability
Proceedings of CS&P, International Workshop on Concurrency, Specification and Programming. Ruciane, Poland. pp 433-444, Warsaw University Press.
Proceedings of LCMAS2
Workshop on Logic and Communication in Multi-Agent Systems. Electronic lecture notes in Theoretical Computer Science. Volume 126.
The complexity of symbolic model checking temporal-epistemic logics
Proceedings of CS&P, International Workshop on Concurrency, Specification and Programming. Ruciane, Poland. pp 421-432, Warsaw University Press.
Bounded Model Checking for Knowledge and Real Time
Proceedings of the 4th International Joint Conference on Autonomous Agents and Multi Agent Systems (AAMAS'05). ACM Press.
Deontic Logic in Computer Science
Special issue of the Journal of Applied Logic. Volume 3, Issues 3-4. Elsevier.
2004
A logic for knowledge, correctness, and real time
Proceedings of the 5th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA V). Springer LNCS.
Bounded model checking for knowledge over real time
Proceedings of Concurrency Specification and Programming (CSP2004). Potsdam, Germany.
Automatic verification of deontic interpreted systems by model checking via OBDDs
Proceedings of the 16th European Conference on Artificial Intelligence (ECAI04). Valencia, Spain.
Bounded model checking for deontic interpreted systems
Proceedings of the 2nd Workshop on Logic and Communication in Multi-Agent Systems (LCMAS04). Nancy, France.
Proceedings of the Seventh International Workshop on Deontic Logic in Computer Science
(DEON04). LNCS Springer volume 3065.
From bounded to unbounded model checking for interpreted systems
Fundamenta Informaticae. Volume 63 (2,3), pp 107-308.
Verification of multiagent systems via unbounded model checking
Proceedings of the 3rd International Joint on Autonomous Agents and Multiagent systems. (AAMAS04). New York, USA. ACM Press.
Symbolic model checking of multi-agent systems via OBDDs: an algorithm and its implementation
Proceedings of the 3rd International Joint on Autonomous Agents and Multiagent systems. (AAMAS04). New York, USA. ACM Press.
Symbolic Model Checking of Deontic Interpreted Systems via OBDDs
Proceedings of the 7th International Workshop on Deontic Logic in Computer Science (DEON04). Madeira, Portugal. Springer LNCS 3065.
Verifying Multi-agent Systems via Unbounded Model Checking
Proceedings of the 3rd NASA Workshop on Formal Approaches to Agent-Based Systems (FAABS III). Washington, USA. Springer LNCS Vol 3228.
Towards model checking for multiagent systems via OBDDs
Proceedings of the 3rd NASA Workshop on Formal Approaches to Agent-Based Systems (FAABS III). Washington, USA. Springer LNCS Vol 3228.
2003
A tableux system for deontic interpreted systems
Proceedings of AI03, 16th Australian Joint Conference on Artificial Intelligence. Perth, Australia. Springer LNCS Vol 2903.
Proceedings of LCMAS
Workshop on Logic and Communication in Multi-Agent Systems. Electronic lecture notes in Theoretical Computer Science. Volume 85.
A logic for ignorance
Electronic Lecture Notes of Theoretical Computer Science, volume 85.
A tool for the specification and verification of epistemic properties in interpreted systems
Electronic Lecture Notes of Theoretical Computer Science. Vol 85.
A formulation of violation, error recovery, and enforcement in the bit transmission problem
Journal of Applied Logic (Selected articles from DEON02 - London). A.J.I. Jones, J. Horty eds. Elsevier. Volume 1. (A previous version of this paper appeared in the proceedings of DEON02).
Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking
Fundamenta Informaticae 55(2), 167–185 (2003).
Ignore at your peril - towards a logic for ignorance
Proceedings of AAMAS03, Second International Conference on Autonomous Agents and Multi-Agent Systems. Melbourne, 2003. Short paper. ACM Press.
Towards model checking interpreted systems
Proceedings of AAMAS03, Second International Conference on Autonomous Agents and Multi-Agent Systems. Melbourne, 2003. Short paper. ACM Press.
Deontic Interpreted Systems
Studia Logica (Special Issue on The Dynamics of Knowledge). W. van der Hoek and M. Wooldridge eds. Kluwer Academic Publishers. Volume 75.
2002
Bounded model checking for interpreted systems: preliminary experimental results
Proceedings of the Second NASA Workshop on Formal Approaches to Agent-Based Systems FAABS II, Greenbelt, MD, USA. Springer Verlag LNCS Vol 2699.
Bounded Model Checking for Interpreted Systems
(extended version). ICS PAS Technical Report 946, 2002. Institute of Computer Science, PAS, 01-237 Warsaw, Poland.
Towards model checking interpreted systems
Proceedings of MoChArt (International Workshop on Model Checking and Artificial Intelligence). Lyon, France.
The bit transmission problem revisited
Proceedings of AAMAS'02 (First International Joint Conference on Autonomous Agents and Multiagent Systems). Bologna, Italy.
Violation, error recovery, and enforcement in the bit transmission problem
Proceedings of DEON'02 (Sixth International Workshop on Deontic Logic in Computer Science). London, UK.
A Classification Scheme for Negotiation in Electronic Commerce
Journal of Group Decision and Negotiation. Kluwer Academic Publishers.
2001
On Multi-agent systems specification via deontic logic
Proceedings of ATAL01, Agent Theories Languages, and Architectures. Seattle. Springer Verlag Lecture Notes in AI vol 2333 (Intelligent Agents VIII).
Extending Interpreted Systems with some Deontic Concepts
Theoretical Aspects of Rationality and Knowledge 2001. Siena, Italy. Morgan Kauffman publishers.
Automated Negotiation: Prospects, Methods, and Challenges
Journal of Group Decision and Negotiation. 10:199-215, 2001. Kluwer Academic Publishers.
A Classification Scheme for Negotiation in Electronic Commerce
LNAI volume 1991: "Agent Mediated Electronic Commerce; A European Perspective". Springer LNAI ©. pp 19-34,
2000
Investigations in grounded semantics for MAS specifications via deontic logic
Imperial College Technical Reports, London.
Multi-Agent VSK Logic
Proceedings of JELIA2000, 7th European Workshop Logic in Artificial Intelligence. Malaga, Spain. Springer LNAI Vol 1919.
A Logic of Visibility, Perception, and Knowledge: Completeness and Correspondence results
Proceedings of FAPR2000, International Conference on Pure and Applied Practical Reasoning. London. A revised version appears on the Logic Journal of the IGPL, Volume 9, Issue 2 (2001).
Knowledge in Multi-Agent Systems: Initial Configurations and Broadcast
ACM Transactions of Computational Logic. Volume 1, Issue 2. ACM Press.
1999
Reasoning about Visibility, Perception, and Knowledge
Proceedings of the sixth international workshop on Agent Theories, Architectures, and Languages (ATAL-99), Springer LNAI © volume 1757.
A spectrum of modes of knowledge sharing between agents
Proceedings of the sixth international workshop on Agent Theories, Architectures, and Languages (ATAL-99), Springer LNAI © volume 1757.
Intelligent Agents
(Guest editor of the special issue of Crossroads). ACM press.
Information Sharing among Ideal Agents
Ph.D. Thesis. School of Computer Science, University of Birmingham.
1998
An algorithmic approach to knowledge evolution
Artificial Intelligence for Engineering Design, Analysis and Manufacturing (AIEDAM), Vol. 13, No. 2 (Special issue on Temporal Logic in Engineering). Cambridge University Press.
Model refinement and model checking for S5n
Proceedings of the ECAI-98 Workshop on Practical Reasoning and Rationality, Brighton (UK).
Ideal agents sharing (some!) knowledge
In Proceedings of ECAI-98, 13th European Conference on Artificial Intelligence. John Wiley & Sons. Brighton (UK).
1997
On the relation between Interpreted Systems and Kripke Models
Proceedings of the AI97 Workshop on Theoretical and Practical Foundation of Intelligent Agents and Agent-Oriented Systems, Perth (WA). Springer LNCS Vol 1441.
A note on the relation between Interpreted Systems and Kripke Models
2nd Workshop on Practical Reasoning and Rationality, Manchester. Expanded version presented at Agent Symposium at ESSLLI97.
Combining Logics for Multi-Agent systems (Abstract)
ModelAge'97, Proceedings of the Esprit WG Workshop. Siena, Italy.
Formalisms for multi-agent systems
The Knowledge Engineering Review, Vol. 12:3, 1997, 315-321. Oxford University Press.
1996
QLB: a quantified logic for belief
Intelligent Agents III, Proceedings of the Third International Workshop on Agent Theories, Architectures, and Languages (ATAL-96). Budapest, Hungary. Springer LNCS Vol 1193.
1995
QLB: una logica predicativa delle credenze. Sintassi, semantica e una procedura di prova automatica dei teoremi
Master's thesis. Politecnico di Milano.
No publications match this filter.