181 results found
Lomuscio A, Solanki M, 2009, Mapping OWL-S processes to multi agent systems: a verification oriented approach, 23rd International Conference on Advanced Information Networking and Applications Workshops, Publisher: IEEE, Pages: 488-493
Cohen M, Dam M, Lomuscio A, et al., 2009, A Data Symmetry Reduction Technique for Temporal-epistemic Logic, 7th International Symposium on Automated Technology for Verification and Analysis, Publisher: SPRINGER-VERLAG BERLIN, Pages: 69-83, ISSN: 0302-9743
Cohen M, Dam M, Russo F, et al., 2009, Abstraction in model checking multi-agent systems, Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, Vol: 1, Pages: 710-717, ISSN: 1548-8403
We present an abstraction technique for multi-agent, systems preserving temporal-epistcrnic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain. Copyright © 2009, International Foundation for Autonomous Agents and Multiagent Systems.
Ezekiel J, Lomuscio A, 2009, Combining fault injection and model checking to verify fault tolerance in multi-agent systems., Publisher: IFAAMAS, Pages: 113-120
Cohen M, Dam M, Lomuscio A, et al., 2009, Abstraction in model checking multi-agent systems., Publisher: IFAAMAS, Pages: 945-952
, 2008, Towards verifying contract regulated service composition, Pages: 254-261
We report on a novel approach to (semi-)automatically compile and verify contract-regulated service compositions. We specify web services and the contracts governing them as WSBPEL behaviours. We compile WSBPEL behaviours into the specialised system description language ISPL, to be used with the model checker MCMAS to verify behaviours automatically. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivating example whose state space is approximately 106 and discuss experimental results. © 2008 IEEE.
, 2008, A complete first-order logic of knowledge and time, Pages: 705-714
We introduce and investigate quantified interpreted systems, a semantics to reason about knowledge and time in a firstorder setting. We provide an axiomatisation, which we show to be sound and complete. We utilise the formalism to study message passing systems (Lamport 1978; Fagin et al 1995) in a first-order setting, and compare the results obtained to those available for the propositional case. Copyright © 2008, Association for the Advancement of Artificial Intelligence.
Lomuscio A, Penczek W, 2008, LDYIS: a Framework for Model Checking Security Protocols, Concurrency Specification and Programming Workshop, Publisher: IOS PRESS, Pages: 359-375, ISSN: 0169-2968
, 2008, Towards verifying compliance in agent-based Web service compositions, Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, Vol: 1, Pages: 262-269, ISSN: 1548-8403
We explore the problem of specification and verification of compliance in agent based Web service compositions. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivating example where the behaviours of participating agents are governed by contracts. The composition is specified in OWL-S and mapped to our chosen formalism. Finally we use an existing symbolic model checker to verify the example specification whose state space is approximately 221 and discuss experimental results. Copyright © 2008, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
Belardinelli F, Lomuscio A, 2008, A Complete Quantified Epistemic Logic for Reasoning about Message Passing Systems, 8th International Workshop on Computational Logic in Multi-Agent Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 248-+, ISSN: 0302-9743
Lomuscio A, Qu H, Solanki M, 2008, Towards verifying compliance in agent-based web service compositions., Publisher: IFAAMAS, Pages: 265-272
, 2007, A quantified epistemic logic for reasoning about multi-agent systems, Pages: 601-603
We investigate quantified interpreted systems, a semantics for multiagent systems in which agents can reason about individuals, their properties, and the relationships among them. We analyse a first-order epistemic language interpreted on this semantics and show soundness and completeness of Q.S5n, an axiomatisation for these structures. © 2007 IFAAMAS.
, 2007, A temporal epistemic logic with a reset operation, Pages: 574-581
We present an axiomatisation for an extension of a temporal epistemic logic with an epistemic "reset" operator defined on the intersection between epistemic and temporal relations. Additionally we show the logic has the finite model property, hence it is decidable. © 2007 IFAAMAS.
, 2007, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 4428 LNAI, ISSN: 0302-9743
Lomuscio A, Penczek W, Wozna B, 2007, Bounded model checking for knowledge and real time, Publisher: ELSEVIER SCIENCE BV, Pages: 1011-1038, ISSN: 0004-3702
Lomuscio A, Penczek W, 2007, Symbolic model checking for temporal-epistemic logics, Pages: 77-77, ISSN: 0163-5700
Lomuscio A, Pecheur C, Raimondi F, 2007, Automatic Verification of Knowledge and Time with NuSMV, 20th International Joint Conference on Artificial Intelligence, Publisher: IJCAI-INT JOINT CONF ARTIF INTELL, Pages: 1384-1389
Lomuscio A, Raimondi F, wozna B, 2007, Verification of the TESLA protocol in MCMAS-X, Workshop on the Concurrency Specification and Programming (CS&P), Publisher: IOS PRESS, Pages: 473-486, ISSN: 0169-2968
Lomuscio A, Wozna B, Zbrzezny A, 2007, Bounded model checking real-time multi-agent systems with clock differences: Theory and implementation, 4th International Workshop on Model Checking and Artificial Intelligence (MoChArt IV), Publisher: SPRINGER-VERLAG BERLIN, Pages: 95-+, ISSN: 0302-9743
Lomuscio A, Qu H, Sergot M, et al., 2007, Verifying temporal and epistemic properties of web service compositions, 5th International Conference on Service-Oriented Computing (ICSOC 2007), Publisher: SPRINGER-VERLAG BERLIN, Pages: 456-+, ISSN: 0302-9743
Edelkamp S, Lomuscio A, 2007, Proceedings of Mochart4, Publisher: Springer
Raimondi F, Lomuscio A, 2007, Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams, Journal of Applied Logic, Vol: 5, Pages: 235-251, ISSN: 1570-8683
, 2007, Model Checking and Artificial Intelligence, 4th Workshop, MoChArt IV, Riva del Garda, Italy, August 29, 2006, Revised Selected and Invited Papers, Publisher: Springer
Lomuscio A, Penczek W, 2007, Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
, 2006, A complete and decidable security-specialised logic and its application to the TESLA protocol, Pages: 145-152
We examine a logic to reason about security protocols by means of temporal and epistemic concepts. We report results on completeness and decidability of the formalism as well as its expressiveness. As a case study we apply the formalism in the analysis of TESLA, a secure stream multi-cast protocol. Copyright 2006 ACM.
, 2006, Model checking knowledge, strategies, and games in multi-agent systems, Pages: 161-168
We present an OBDD-based methodology for verifying time, knowledge, and strategies in multi-agent systems specified by the formalism of interpreted systems. To this end, we investigate the interpretation of ATL and epistemic formulae in various classes of interpreted systems, we present model checking algorithms and their implementation, and report experimental results. Copyright 2006 ACM.
, 2006, On the complexity of practical ATL model checking, Pages: 201-208
We investigate the computational complexity of reasoning about multi-agent systems using the cooperation logic ATL of Alur, Henzinger, and Kupferman. It is known that satisfiability checking is EXPTIME-complete for "full" ATL, and PSPACE-complete (in the general case) for the fragment of ATL corresponding to Pauly's Coalition Logic. In contrast, the model checking problems for ATL and Coalition Logic can both be solved in time polynomial in the size of the formula and the size of model against which the formula is to be checked. However, these latter results assume an extensive representation of models, in which all states of a model are explicitly enumerated. Such representations are not feasible in practice. In this paper we investigate the complexity of the ATL and Coalition Logic model checking problems for a more "reasonable" model representation known as SRML ("Simple Reactive Modules Language"), a simplified version of the actual model representation languages used for model checkers such as SMV and MOCHA. While it is unsurprising that, when measured against such representations, the model checking problems for ATL and Coalition Logic have a higher complexity than when measured against explicit state representations, we show that in fact the ATL and Coalition Logic model checking problems for SRML models have the same complexity as the corresponding satisfiability problems. That is, model checking ATL formulae against SRML models is EXPTIME-complete, and model checking Coalition Logic formulae against SRML models is PSPACE-complete. We conclude by investigating some technical issues around these results, and discussing their implications. Copyright 2006 ACM.
Lomuscio AR, Pecheur C, Raimondi F, 2006, Verification of knowledge and time with NuSMV., Twentieth International Conference on Artificial Intelligence
Kacprzak M, Lomuscio A, Niewiadomski A, et al., 2006, Comparing BDD and SAT based techniques for model checking Chaum's dining cryptographers protocol, Meeting on Concurrency Specification and Programming, Publisher: IOS PRESS, Pages: 215-234, ISSN: 0169-2968
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.