Mads Dam

IJCAI Conference 2009 Conference Paper

• Mika Cohen
• Mads Dam
• Alessio Lomuscio
• Hongyang Qu

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.

AAMAS Conference 2009 Conference Paper

Abstraction in Model Checking Multi-Agent Systems

• Mika Cohen
• Mads Dam
• Alessio Lomuscio

We present an abstraction technique for multi-agent systems preserving temporal-epistemic 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.

I&C Journal 1998 Journal Article

Proving Properties of Dynamic Process Networks

• Mads Dam

We present the first compositional proof system for checking processes against formulas in the modalμ-calculus which is capable of handling dynamic process networks. The proof system is obtained in a systematic way from the operational semantics of the underlying process algebra. A non-trivial proof example is given, and the proof system is shown to be sound in general, and complete for finite-state processes.

TCS Journal 1997 Journal Article

On the decidability of process equivalences for the π-calculus

• Mads Dam

We present general results for showing process equivalences applied to the finite control fragment of the π-calculus decidable. Firstly, a Finite Reachability Theorem states that up to finite name spaces and up to a static normalisation procedure, the set of reachable agent expressions is finite. Secondly, a Boundedness Lemma shows that no potential computations are missed when name spaces are chosen large enough, but finite. We show how these results lead to decidability for a number of π-calculus equivalences such as strong or weak, late or early bismulation equivalence. Furthermore, for strong late equivalence we show how our techniques can be used to adapt the well-known Paige-Tarjan algorithm. Strikingly, this results in a single exponential running time not much worse than the running time for the case of for instance CCS. Our results considerably strengthens previous results on decidable equivalences for parameter-passing process calculi.

I&C Journal 1996 Journal Article

Model Checking Mobile Processes

• Mads Dam

We introduce a temporal logic for the polyadicπ-calculus based on fixed point extensions of Hennessy–Milner logic. Features are added to account for parametrisation, generation, and passing of names, including the use, following Milner, of dependent sum and product to account for (unlocalised) input and output, and explicit parametrisation on names usingλ-abstraction and application. The latter provides a single name binding mechanism supporting all parametrisation needed. A proof system and decision procedure is developed based on Stirling and Walker's approach to model checking the modalμ-calculus using constants. One difficulty, for both conceptual and efficiency-based reasons, is to avoid the explicit use of theω-rule for parametrised processes. A key idea, following Hennessy and Lin's approach to deciding bisimulation for certain types of value-passing processes, is the relativisation of correctness assertions to conditions on names. Based on this idea, a proof system and a decision procedure are obtained for arbitraryπ-calculus processes with finite control, π-calculus correlates of CCS finite-state processes, avoiding the use of parallel composition in recursively defined processes.

TCS Journal 1994 Journal Article

CTL∗ and ECTL∗ as fragments of the modal μ-calculus

• Mads Dam

Direct embeddings of the full branching-time CTL∗ and its extension ECTL∗ into the modal μ-calculus are presented. The embeddings use tableaux as intermediate representations of formulas, and use extremal fixed points to characterise those paths through tableaux that satisfy an admissibility criterion, guaranteeing eventualities to be eventually satisfied. The version of ECTL∗ considered replaces the entire linear-time fragment of CTL∗ by Büchi automata on infinite strings. As a consequence the embedding of ECTL∗ turns out to be computable in linear time, while the embedding of CTL∗ is doubly exponential in the worst case.