Fundamenta Informaticae - Volume 140, issue 1

Article Type: Other

DOI: 10.3233/FI-2015-1242

Citation: Fundamenta Informaticae, vol. 140, no. 1, pp. v-vi, 2015

Authors: Baldan, Paolo | Carraro, Alberto

Article Type: Research Article

Abstract: The concept of non-interference has been introduced to characterise the absence of undesired information flows in a computing system. Although it is often explained referring to an informal notion of causality - the activity involving the part of the system with higher level of confidentiality should not cause any observable effect at lower levels - it is almost invariably formalised in terms of interleaving semantics. Here we focus on Petri nets and on the BNDC (Bisimilarity-based Non-Deducibility on Composition) property, a formalisation of non-interference widely studied in the literature. We show that BNDC admits natural characterisations based on the unfolding …semantics - a classical true concurrent semantics for Petri nets - in terms of causalities and conflicts between high and low level activities. This leads to algorithms for checking BNDC on various classes of Petri nets, based on the construction of suitable complete prefixes of the unfolding. We also developed a prototype tool UBIC (Unfolding-Based Interference Checker), working on safe Petri nets, which provides promising results in terms of efficiency. Show more

Keywords: Petri nets, non-interference, bisimilarity-based non-deducibility on composition (BNDC), unfolding, true concurrency, verification

DOI: 10.3233/FI-2015-1243

Citation: Fundamenta Informaticae, vol. 140, no. 1, pp. 1-38, 2015

Authors: Best, Eike | Devillers, Raymond

Article Type: Research Article

Abstract: This paper presents a dedicated Petri net synthesis algorithm for the case that a transition system is finite, live, and persistent. In particular, the paper delineates exactly when and how a structurally persistent net may be constructed, by crystallising, out of a general region-theoretic approach, a minimised set of simplified systems of linear inequalities. This extends previous results where reversibility, instead of liveness, played an important role.

Keywords: Cyclic Behaviour, Persistence, Labelled Transition Systems, Liveness, Parikh Vectors, Petri Nets, Region Theory, System Synthesis

DOI: 10.3233/FI-2015-1244

Citation: Fundamenta Informaticae, vol. 140, no. 1, pp. 39-59, 2015

Authors: Avellaneda, Florent | Morin, Rémi

Article Type: Research Article

Abstract: Checking the structural boundedness and the structural termination of vector addition systems with states boils down to detecting pathological cycles. As opposed to their non-structural variants which require exponential space, these properties need polynomial time only. The algorithm searches for a counter-example in the form of a multiset of arcs computed by means of linear programming. Yet the minimal length of a pathological cycle can be exponential in the size of the system which makes it difficult to visualize and to analyze the detected bug in details. We propose to describe pathological cycles in the form of particular cycles …called flowers. The latter are made of petals which are iterated circuits connected by simple paths that form a calyx. We present an algorithm that builds in polynomial time a flower from the multiset of arcs that represents a pathological cycle. Interestingly the number of petals within a flower is at most equal to the dimension of vectors which helps to describe in a concise way the underlying bug and to analyse it. Show more

Keywords: Vector addition system with states, structural properties, counter-example, dynamic graph, zero-cycle

DOI: 10.3233/FI-2015-1245

Citation: Fundamenta Informaticae, vol. 140, no. 1, pp. 61-87, 2015

Authors: Mateo, José Antonio | Srba, Jiří | Sørensen, Mathias Grund

Article Type: Research Article

Abstract: Analysis of workflow processes with quantitative aspects like timing is of interest in numerous time-critical applications. We suggest a workflow model based on timed-arc Petri nets and study the foundational problems of soundness and strong (time-bounded) soundness. We first consider the discrete-time semantics (integer delays) and explore the decidability of the soundness problems and show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable. For general timed-arc workflow nets soundness and strong soundness become undecidable, though we can design efficient verification algorithms for the subclass of bounded nets. We also discuss the soundness problem in …the continuous-time semantics (real-number delays) and show that for nets with nonstrict guards (where the reachability question coincides for both semantics) the soundness checking problem does not in general follow the approach for the discrete semantics and different zone-based techniques are needed for introducing its decidability in the bounded case. Finally, we demonstrate the usability of our theory on the case studies of a Brake System Control Unit used in aircraft certification, the MPEG2 encoding algorithm, and a blood transfusion workflow. The implementation of the algorithms is freely available as a part of the model checker TAPAAL (www.tapaal.net). Show more

Keywords: timed workflow processes, soundness checking, decidability, verification

DOI: 10.3233/FI-2015-1246

Citation: Fundamenta Informaticae, vol. 140, no. 1, pp. 89-121, 2015