Knowledge Dynamics and Behavioural Equivalencesin Multi-Agent Systems

We define a process calculus to describe multi-agent systems with timeouts for communication and mobility able to handle knowledge. The knowledge of an agent is represented as sets of trees whose nodes carry information; it is used to decide the interactions with other agents. The evolution of the system with exchanges of knowledge between agents is presented by the operational semantics, capturing the concurrent executions by a multiset of actions in a labelled transition system. Several results concerning the relationship between the agents and their knowledge are presented. We introduce and study some specific behavioural equivalences in multi-agent systems, including a knowledge equivalence able to distinguish two systems based on the interaction of the agents with their local knowledge.

Relating Apartness and Bisimulation

A bisimulation for a coalgebra of a functor on the category of sets can be described via a coalgebra in the category of relations, of a lifted functor. A final coalgebra then gives rise to the coinduction principle, which states that two bisimilar elements are equal. For polynomial functors, this leads to well-known descriptions. In the present paper we look at the dual notion of "apartness". Intuitively, two elements are apart if there is a positive way to distinguish them. Phrased differently: two elements are apart if and only if they are not bisimilar. Since apartness is an inductive notion, described by a least fixed point, we can give a proof system, to derive that two elements are apart. This proof system has derivation rules and two elements are apart if and only if there is a finite derivation (using the rules) of this fact. We study apartness versus bisimulation in two separate ways. First, for weak forms of bisimulation on labelled transition systems, where silent (tau) steps are included, we define an apartness notion that corresponds to weak bisimulation and another apartness that corresponds to branching bisimulation. The rules for apartness can be used to show that two states of a labelled transition system are not branching bismilar. To support the apartness view on labelled transition systems, we cast a number of well-known properties of branching bisimulation in terms of branching apartness and prove them. Next, we also study the more general categorical situation and show that indeed, apartness is the dual of bisimilarity in a precise categorical sense: apartness is an initial algebra and gives rise to an induction principle. In this analogy, we include the powerset functor, which gives a semantics to non-deterministic choice in process-theory.

An Innovative Prostate Cancer Detection Method via Model Checking

Purpose: one of typical cancer among men is the prostate tumour. This is the reason why the screening and the early detection is a crucial task to obtain a diagnosis and a subsequent therapy in the shortest possible time. Materials and Methods: in this paper, with the aim to help radiologists and pathologists for a prompt diagnosis, a method for detecting prostate cancer is proposed. Our analysis starts from the magnetic resonances images (coronal and axial planes), building a labelled transition system for coronal slices and another one for axial, which takes into account a number of non invasive radiomic features. Thus, a set of formulae in temporal logic characterizing the prostate cancer is verified through the model checking technique, to detect the prostate cancer. The proposed method considers magnetic resonance images without the Region Of Interest. This represents one of the major novelty of the method. Results: the proposed method is evaluated on a data-set composed of 40 patients, obtaining very interesting performances in the discrimination between affected and not affected prostate cancer patients. Conclusion: the study confirms the effectiveness of the formal methods to discriminate between cancerous and benign prostate MRIs with a method not requiring the ROI of the cancerous area, by obtaining a sensitivity and a specificity equal to 1.

Who is obliged when many are involved? Labelled transition system modelling of how obligation arises

The paper tackles the problem of the relation between rights and obligations. Two examples of situations in which such a relation occurs are discussed. One concerns the abortion regulations in Polish law, the other one—a clash between freedom of expression and freedom of enterprise occurring in the context of discrimination. The examples are analysed and formalised using labelled transition systems in the $$n\mathcal {C}+$$ n C + framework. Rights are introduced to the system as procedures allowing for their fulfilment. Obligations are based on the requirement of cooperation in the realisation of the goals of the agent that has a right. If the right of an agent cannot be fulfilled without an action of another agent, then that action is obligatory for that agent. If there are many potential contributors who are individually allowed to refuse, then the last of them is obliged to help when all the others have already refused. By means of formalisation this account of the relation under consideration is precisely expressed and shown consistent.

Target-oriented Petri Net Synthesis

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

Target-oriented Petri Net Synthesis

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

Verification of Compliance for Multilevel Models in Individual Trace Semantics

The paper considers the problem of verification of compliance between models representing the same system on different level of abstraction. The existing approaches are mostly based on refinement relation. But the models representing industrial systems are quite big and complex, while semantics gap between the level is quite big. As a result, the existing methods became too complex and labour intensive. The paper presents new verification techniques that targets to prove multimodel compliance in terms of individual trace semantics. The techniques assume that each model is verified, i.e. it is proved that starting from initial states of labelled transition system is not possible to reach unsafe states by using valid transitions. The first proposed technique allows to prove that the detailed model satisfies to requirements of the abstract model, i.e. reachable states of detailed model do not include states corresponding to unsafe states of the abstract model. The second proposed technique allows to prove that the detailed model satisfies to behaviour specification of the abstract model, i.e. all reachable transitions of the detailed model do not include transitions corresponding to invalid transitions of the abstract model. For each technique the correspondence relation is defined in terms of the models, i.e. the relations are formally defined and they can be used for analysis with interactive or automated provers. At the same time, there are some requirements to that relations that are expressed in terms of low level events that exist hypothetically only and can be analyzed theoretically only. As a result, the proposed techniques provides a reasonable approach to prove compliance between mulilevel models in more approachable way for industrial settings.

An Axiomatic Approach to Reversible Computation

Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between these properties. In particular, we show how they are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new notions related to causal consistent reversibility, namely causal safety and causal liveness, and show that they are derivable from our axioms.

Verification of Compliance for Multilevel Models in Individual Trace Semantics

The paper considers the problem of verification of compliance between models representing the same system on different level of abstraction. The existing approaches are mostly based on refinement relation. But the models representing industrial systems are quite big and complex, while semantics gap between the level is quite big. As a result, the existing methods became too complex and labour intensive. The paper presents new verification techniques that targets to prove multimodel compliance in terms of individual trace semantics. The techniques assume that each model is verified, i.e. it is proved that starting from initial states of labelled transition system is not possible to reach unsafe states by using valid transitions. The first proposed technique allows to prove that the detailed model satisfies to requirements of the abstract model, i.e. reachable states of detailed model do not include states corresponding to unsafe states of the abstract model. The second proposed technique allows to prove that the detailed model satisfies to behaviour specification of the abstract model, i.e. all reachable transitions of the detailed model do not include transitions corresponding to invalid transitions of the abstract model. For each technique the correspondence relation is defined in terms of the models, i.e. the relations are formally defined and they can be used for analysis with interactive or automated provers. At the same time, there are some requirements to that relations that are expressed in terms of low level events that exist hypothetically only and can be analyzed theoretically only. As a result, the proposed techniques provides a reasonable approach to prove compliance between mulilevel models in more approachable way for industrial settings.

Modelling the Embedded Control System Using iUML-B Pattern State Machine

Developing the formal model based on the Event-B design pattern is an excellent method to improve the development efficiency of the embedded control system and improve the reusability of the formal model. However, the instantiation of the Event-B design pattern requires the manual writing of a large number of model codes, which brings a great deal of learning cost and coding burden to the engineering staff. In this paper, we propose a modelling approach for formal development of control systems based on the application of iUML-B state machine patterns to model the four synchronization patterns of the typical control system. Then, we use the instantiation of iUML-B pattern state machine to establish a typical multilevel control system's Event-B model. The simulation results show that the event trace of the model obtained using our method is the same as that of the corresponding model obtained using the traditional Event-B design pattern. Compared with the traditional Event-B design pattern method, our method can greatly reduce the manual coding burden in the modelling process. The system model expressed using the iUML-B pattern state machine can be easily mapped to the labelled transition system so as to verify the behavioural properties of the model.