Search

This paper presents a framework, called VerifCar, devoted to the validation of decision policies of communicating autonomous vehicles (CAVs). The approach focuses on the formal modeling of CAVs by means of timed automata, allowing a formal and exhaustive analysis of the behaviors of vehicles. VerifCar supports a parametric modeling of CAV systems as a network of timed automata tailored for verification and limiting the well-known state space explosion. As an illustration, VerifCar is applied to check robustness and efficiency, as well as to asses the impact of communication delays on the decision algorithms of CAVs, on well chosen case studies representing real-life critical situations. [ABSTRACT FROM AUTHOR]

This paper describes a synthesis procedure dedicated to the construction of choice-free Petri nets from finite persistent transition systems, whenever possible. Taking advantage of the properties of choice-free Petri nets, a two-step approach is proposed. A pre-synthesis step checks necessary structural properties of the transition system and constructs some data structures needed for the second step. Then, a minimised set of simplified systems of linear inequalities is distilled from a general region-theoretic approach. This leads to a substantial narrowing of the sets of states for which linear inequalities must be solved, and allows an early detection of failures, supported by constructive error messages. The performance of the resulting algorithm is measured and compared numerically with existing synthesis tools. [ABSTRACT FROM AUTHOR]

It is well-known that the reachability graph of a sum of disjoint Petri nets is the disjoint product of the reachability graphs of the components. We shall consider here the converse problem, i.e., determine when and how a transition system may be decomposed in non-trivial concurrent factors, and extend the theory to more general labelled transition systems. Meanwhile, we shall develop interesting algebraic properties of disjoint products. The present paper is an extended version of Devillers (in: Desel, Yakovlev (eds) Proceedings 16th international conference on application of concurrency to system design (ACSD 2016), 2016). [ABSTRACT FROM AUTHOR]

T-systems are generalisations of marked graph Petri nets. This paper describes synthesis algorithms that allow bounded or unbounded T-systems to be derived from finite or infinite labelled transition systems satisfying a set of necessary properties. These properties can thus be interpreted as axioms characterising T-system state spaces. [ABSTRACT FROM AUTHOR]

In formal verification, a structural object, such as a program or a Petri net, is given, and questions are asked about its behaviour. In system synthesis, conversely, a behavioural object, such as a transition system, is given, and questions are asked about the existence of a structural object realising this behaviour. In system reengineering, one wishes to transform a given system into another one, with similar behaviour and other properties not enjoyed by the original system. This paper addresses synthesis and reengineering problems in the specific framework of finite-state labelled transition systems, place/transition Petri nets, and behaviour isomorphisms. Since algorithms solving these problems are prohibitively time-consuming in general, it is interesting to know whether they can be improved in restricted circumstances, and whether direct correspondences can be found between classes of behavioural and classes of structural objects. This paper is concerned with persistent systems, which occur in hardware design and in various other applications. We shall derive exact conditions for a finite persistent transition system to be isomorphically implementable by a bounded Petri net exhibiting persistence in a structural way, and derive an efficient algorithm to find such a net if one exists. For the class of marked graph Petri nets, this leads to an exact characterisation of their state spaces. [ABSTRACT FROM AUTHOR]

This paper shows how to define Petri nets through recursive equations. It specifically addresses this problem within the context of the {it box algebra}, a model of concurrent computation which combines Petri nets and standard process algebras. The paper presents a detailed investigation of the solvability of recursive equations on nets in what is arguably the most general setting. For it allows an infinite number of possibly unguarded equations, each equation possibly involving infinitely many recursion variables. The main result is that by using a suitable partially ordered domain of nets, it is always possible to solve a system of equations by constructing the limit of a chain of successive approximations. [ABSTRACT FROM AUTHOR]

The paper shows how to synthesise S-invariants and S-components for Petri Boxes constructed through general recursions, from S-invariants/S-components of their constituents. The construction is based on the tree-structure of the interface places used to define this operator and extends similar results obtained for the refinement operator. Emphasis is put on deriving coverability results; these results are then used to show that all the nets obtained through refinements and recursions from a family covered by S-components are self-concurrency free, at most 2-safe and exhibit a generalised emptiness property; in particular, this is the case for the nets obtained in the translation of the process algebra of Box expressions. [ABSTRACT FROM AUTHOR]

After various attempts, an equivalence relation is defined for labelled Petri nets, on the base of the concurrency semantics of net theory. This relation, called Fully Concurrent bisimulation and abbreviated FC-bisimulation, preserves the level of concurrency of visible operations and, under some conditions, allows to enforce injective labelling on them. Refinements of a visible operation are also defined and we show that, under some conditions, they preserve FC-bisimulation. [ABSTRACT FROM AUTHOR]