Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
IS Journal 2015 Journal Article
Developing and implementing a model checker dedicated to conditional logic with the user interface are urgent requirements for determining whether agents comply with their commitment protocols.
I&C Journal 2015 Journal Article
Alternating-time Temporal Logic is a logic to reason about strategies that agents can adopt to achieve a specified collective goal. A number of extensions for this logic exist; some of them combine strategies and partial observability, some others include fairness constraints, but to the best of our knowledge no work provides a unified framework for strategies, partial observability and fairness constraints. Integration of these three concepts is important when reasoning about the capabilities of agents without full knowledge of a system, for instance when the agents can assume that the environment behaves in a fair way. We present ATLK irF, a logic combining strategies under partial observability in a system with fairness constraints on states. We introduce a model-checking algorithm for ATLK irF by extending the algorithm for a full-observability variant of the logic and we investigate its complexity. We validate our proposal with an experimental evaluation.
TCS Journal 2014 Journal Article
We consider models of programs that incorporate probability, dense real-time and data. We present a new abstraction refinement method for computing minimum and maximum reachability probabilities for such models. Our approach uses strictly local refinement steps to reduce both the size of abstractions generated and the complexity of operations needed, in comparison to previous approaches of this kind. We implement the techniques and evaluate them on a selection of large case studies, including some infinite-state probabilistic real-time models, demonstrating improvements over existing tools in several cases.
I&C Journal 2013 Journal Article
Compositional approaches to verification offer a powerful means to address the challenge of scalability. In this paper, we develop techniques for compositional verification of probabilistic systems based on the assume-guarantee paradigm. We target systems that exhibit both nondeterministic and stochastic behaviour, modelled as probabilistic automata, and augment these models with costs or rewards to reason about, for example, energy usage or performance metrics. Despite significant theoretical advances in compositional reasoning for probabilistic automata, there has been a distinct lack of practical progress regarding automated verification. We propose a new assume-guarantee framework based on multi-objective probabilistic model checking which supports compositional verification for a range of quantitative properties, including probabilistic ω-regular specifications and expected total cost or reward measures. We present a wide selection of assume-guarantee proof rules, including asymmetric, circular and asynchronous variants, and also show how to obtain numerical results in a compositional fashion. Given appropriate assumptions to be used in the proof rules, our compositional verification methods are, in contrast to previously proposed approaches, efficient and fully automated. Experimental results demonstrate their practical applicability on several large case studies, including instances where conventional probabilistic verification is infeasible.
Highlights Conference 2013 Conference Abstract
AAMAS Conference 2013 Conference Paper
Social commitments provide a powerful representation for modeling multi-agent interactions without relinquishing part of agents autonomy and flexibility. However, distinguishing between different but related types of conditional commitments, a natural frame of social commitments, is not considered yet. In this paper, we define a new logical language, CTLcc, which extends CTL with modalities to represent conditional commitments and their fulfillments using the formalism of interpreted systems. Such a language excludes the paradox that plagues the semantics of fulfilling commitments in the literature. We present a set of rules to reason about conditional commitments and their fulfillments.
AAMAS Conference 2011 Conference Paper
Social commitments have been widely studied to represent business contracts among agents with different competing objectives in communicating multi-agent systems. However, their formal verification is still an open issue. This paper proposes a novel model-checking algorithm to address this problem. We define a new temporal logic, CTLC, which extends CTL with modalities for social commitments and their fulfillment and violation. The verification technique is based on symbolic model checking that uses ordered binary decision diagrams to give a compact representation of the system. We also prove that the problem of model checking CTLC is polynomial-time reducible to the problem of model checking CTLK, the combination of CTL with modalities for knowledge. We finally present the full implementation of the proposed algorithm by extending the MCMAS symbolic model checker and report on the experimental results obtained when verifying the NetBill protocol.
AAMAS Conference 2010 Conference Paper
We investigate partial order reduction for model checking multi-agent systems by focusing on interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed in the system. We present a notion of stuttering-equivalence, and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model checking step and show preservation properties. We evaluate the technique by discussing implementations and the experimental results obtained against well-known examples in the MAS literature.
JAAMAS Journal 2010 Journal Article
Abstract We report on a novel approach to (semi-)automatically compile and verify contract-regulated service compositions implemented as multi-agent systems. We model web service behaviours and the contracts governing them as WSBPEL specification. We use the formalism of temporal-epistemic logic, suitably extended to deal with compliance/violations of contracts, to specify properties of service compositions. We compile the WSBPEL behaviours into a specialised system description language ISPL, to be used with the model checker MCMAS to verify the behaviours automatically. We illustrate these concepts using a motivating example whose state space is approximately 10 6 and discuss experimental results.
IJCAI Conference 2009 Conference Paper
We introduce a symmetry reduction technique for model checking temporal-epistemic properties of multi-agent systems defined in the mainstream interpreted systems framework. The technique, based on counterpart semantics, aims to reduce the set of initial states that need to be considered in a model. We present theoretical results establishing that there are neither false positives nor false negatives in the reduced model. We evaluate the technique by presenting the results of an implementation tested against two well known applications of epistemic logic, the muddy children and the dining cryptographers. The experimental results obtained confirm that the reduction in model checking time can be dramatic, thereby allowing for the verification of hitherto intractable systems.
TCS Journal 2008 Journal Article
This paper presents an automatic method for calculating the path condition for programs with real time constraints. We model concurrent systems using timed transition systems and translate them into extended timed automata. Then an acyclic extended timed automaton is constructed and the path condition is calculated backwards over it. This method can be used for semiautomatic verification of a unit of code in isolation, i. e. , without providing the exact values of parameters with which it is called. It can also be used for test case generation for real-time systems. Such a symbolic model checking algorithm was implemented previous in the PET system [E. Gunter, D. Peled, Unit checking: Symbolic model checking for a unit of code, Verification: Theory and Practice 2003, Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday, Lecture Notes in Computer Science, vol. 2772, Springer, 548–567] for untimed systems. Our method can also be used for the automatic generation of test cases for unit testing. The current generalization of the calculation of path condition for the timed case turns out to be quite tricky, since not only the selected path contributes to the path condition, but also timing constraints of alternative choices in the code.
AAMAS Conference 2008 Conference Paper
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.