Multi-valued Verification of Strategic Ability

in Fundamenta Informaticae (2020), 175(1-4), 207-251

Some multi-agent scenarios call for the possibility of evaluating specifications in aricher domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an ... [more ▼]

Some multi-agent scenarios call for the possibility of evaluating specifications in aricher domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued alternating-time temporal logic(mv-ATL∗→), an expressive logic to specify strategic abilities in multi-agent systems. It is well known that, for branching-time logics, a general method for model-independent translation from multi-valued to two-valued model checking exists. We show that the method cannot be directly extended to mv-ATL∗→. We also propose two ways of overcoming the problem. Firstly, we identify constraints on formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL∗→. We show that, in all cases, the complexity of verification increases only linearly when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL∗→and motivate its use for model checking multi-agent systems. [less ▲]

Semantics for specialising attack trees based on linear logic

in Fundamenta Informaticae (2017), 153(1-2), 57-86

Attack trees profile the sub-goals of the proponent of an attack. Attack trees have a variety of semantics depending on the kind of question posed about the attack, where questions are captured by an ... [more ▼]

Attack trees profile the sub-goals of the proponent of an attack. Attack trees have a variety of semantics depending on the kind of question posed about the attack, where questions are captured by an attribute domain. We observe that one of the most general semantics for attack trees, the multiset semantics, coincides with a semantics expressed using linear logic propositions. The semantics can be used to compare attack trees to determine whether one attack tree is a specialisation of another attack tree. Building on these observations, we propose two new semantics for an extension of attack trees named causal attack trees. Such attack trees are extended with an operator capturing the causal order of sub-goals in an attack. These two semantics extend the multiset semantics to sets of series-parallel graphs closed under certain graph homomorphisms, where each semantics respects a class of attribute domains. We define a sound logical system with respect to each of these semantics, by using a recently introduced extension of linear logic, called MAV , featuring a non-commutative operator. The non-commutative operator models causal dependencies in causal attack trees. Similarly to linear logic for attack trees, implication defines a decidable preorder for specialising causal attack trees that soundly respects a class of attribute domains. [less ▲]

Reducibility proofs in the lambda-calculus

in Fundamenta Informaticae (2012), 121

On Realisability Semantics for Intersection Types with Expansion Variables.

in Fundamenta Informaticae (2012), 121

Nuovo DRM Paradiso: Designing a Secure, Verified, Fair Exchange DRM Scheme

in Fundamenta Informaticae (2008), 89(4), 393-417

A process specification formalism

in Fundamenta Informaticae (1990), XIII