Search

Data Nets are a version of colored Petri nets in which tokens carry data from an infinite and linearly ordered domain. This is a very expressive class, though coverability and termination remain decidable. Those problems have recently been proven complete for the F ω ω ω class in the fast growing complexity hierarchy. We characterize the exact complexity of Unordered Data Nets (UDN), a subclass of Data Nets with unordered data. We bound the length of bad sequences in well-quasi orderings of multisets over tuples of naturals by adapting the analogous result by Schmitz and Schnoebelen for words over a finite alphabet. These bounds imply that both problems are in F ω ω . We prove that this result is tight by constructing UDN that weakly compute fast-growing functions and their inverses. This is the first complete problem for F ω ω with an underlying wqo not based on finite words over a finite alphabet.

A general theory introducing asymptotic complexity to testing is presented. Our goal is measuring how fast the effort of testing must increase to reach higher levels of partial certainty on the correctness of the implementation under test (IUT). By recent works it is known that, for many practical testing scenarios, any partial level of correctness certainty less than 1 (where 1 means full certainty) can be reached by some finite test suite. In this paper we address the problem of finding out how fast must these test suites grow as long as the target level gets closer to 1. More precisely, we want to study how test suites grow with α, where α is the inverse of the distance to 1 (e.g., if α = 4 then our target level is 0.75 = 1 − 1 4 ). A general theory to measure this testing complexity is developed. We use this theory to analyze the testing complexity of some general testing problems, as well as the complexity of some specific testing strategies for these problems, and discover that they are within e.g., O ( l o g α ) , O ( l o g 2 α ) , O ( α ) , O ( α l o g α ) , or O ( α ) . Similarly as the computational complexity theory conceptually distinguishes between the complexity of problems and algorithms, tightly identifying the complexity of a testing problem will require reasoning about any testing strategy for the problem. The capability to identify testing complexities will provide testers with a measure of the productivity of testing, that is, a measure of the utility of applying the ( n + 1 ) -th planned test case (after having passed the n previous ones) in terms of how closer would that additional test case get us to the (ideal) complete certainty on the IUT (in-)correctness.

Transient secure association has been widely accepted as a possible alternative to traditional authentication in the context of Ubiquitous Computing. Two components in a distributed system with transient secure association may share a master-slave relationship, which creates a hierarchical but dynamic structure of components. In this paper we develop several formal models for distributed systems with transient secure association, with incremental expressive power, all based on Petri nets. The first model, that we call transient secure association (TSA) systems, considers finitely many components. Then we consider a small extension of TSA systems, in which slaves are initialized whenever a master-slave relation is broken. Last, we define unbounded TSA (uTSA) systems, for which the number of components is not bounded. For each of the defined formalisms, we establish a link to a known class of Petri nets, thus inheriting the corresponding (un)decidability results from them.

We combine two of the existing approaches to the study of concurrency by means of multiset rewriting: multiset rewriting with existential quantification (MSR) and constrained multiset rewriting. We obtain ν-MSR, where we rewrite multisets of atomic formulae, in which terms can only be pure names, where some names can be restricted. We consider the subclass of depth-bounded ν-MSR, for which the interdependence of names is bounded. We prove that they are strictly Well Structured Transition Systems, so that coverability, termination and boundedness are all decidable for depth-bounded ν-MSR. This allows us to obtain new verification results for several formalisms with name binding that can be encoded within ν-MSR, namely polyadic ν-PN (Petri nets with tuples of names as tokens), the π-calculus, MSR or Mobile Ambients.

We prove several decidability and undecidability results for ν-PN, an extension of P/T nets with pure name creation and name management. We give a simple proof of undecidability of reachability, by reducing reachability in nets with inhibitor arcs to it. Thus, the expressive power of ν-PN strictly surpasses that of P/T nets. We encode ν-PN into Petri Data Nets, so that coverability, termination and boundedness are decidable. Moreover, we obtain Ackermann-hardness results for all our decidable decision problems. Then we consider two properties, width-boundedness and depth-boundedness, that factorize boundedness. Width-boundedness has already been proven to be decidable. Here we prove that its complexity is also non-primitive recursive. Then we prove undecidability of depth-boundedness. Finally, we prove that the corresponding “place version” of all the boundedness problems is undecidable for ν-PN. These results carry over to Petri Data Nets.

Mobile Synchronizing Petri Nets (MSPN's) are a model for mobility and coordination based on coloured Petri Nets, in which systems are composed of a collection of (possibly mobile) hardware devices and mobile agents, both modelled homogenously. In this paper we approach their verification, for which we have chosen to code MSPN's into rewriting logic. In order to obtain a representation of MSPN systems by means of a rewrite theory, we develop a class of them, that we call ν-Abstract Petri nets (ν-APN's), which are easily representable in that framework. Moreover, the obtained representation provides a local mechanism for fresh name generation. Then we prove that, even if ν-APN's are a particular class of MSPN systems, they are strong enough to capture the behaviour of any MSPN system. We have chosen Maude to implement ν-APN's, as well as the translation from MSPN's to ν-APN's, for which we make intensive use of its reflective features.

International audience; We characterize the importance of resources (like counters, channels, or alphabets) when measuring the expressiveness of Well-Structured Transition Systems (WSTS). We establish, for usual classes of well partial orders, the equivalence between the existence of order reflections (non-monotonic order embeddings) and the simulations with respect to coverability languages. We show that the non-existence of order reflections can be proved by the computation of order types. This allows us to extend the current classification of WSTS, in particular solving some open problems, and to unify the existing proofs.

We apply language theory to compare the expressive power of infinite-state models that extend Petri nets with features like coloured tokens and/or whole place operations. Specifically, we consider extensions of Petri nets in which tokens carry pure names dynamically generated with special @n-transitions (@n-PN) and compare their expressiveness with transfer and reset nets with black indistinguishable tokens (Affine Well-Structured Nets), and nets in which tokens carry data taken from a linearly ordered domain (Data nets and CMRS). All these models are well-structured transition systems. In order to compare these models we consider the families of languages they recognize, using coverability as the accepting condition. With this criterion, we prove that @n-PNs are in between AWNs and Data Nets/CMRS, but equivalent to an extension of @n-PN with whole-place operations. These results extend the currently known classification of the expressive power of well-structured transition systems. Finally, we study several problems regarding (coverability) languages of AWN and @n-PN.

To the best of our knowledge, we characterize for the first time the importance of resources (counters, channels, alphabets) when measuring expressiveness of WSTS. We establish, for usual classes of wpos, the equivalence between the existence of order reflections (nonmonotonic order embeddings) and the simulations with respect to coverability languages. We show that the non-existence of order reflections can be proved by the computation of order types. This allows us to solve some open problems and to unify the existing proofs of the WSTS classification.

International audience; Workflow Petri nets (wf-nets) are an important formalism for the modeling of business processes. For them we are typically interested in the soundness problem, that intuitively consists in deciding whether several concurrent executions can always terminate properly. Resource-Constrained Workflow Nets (rcfw-nets) are wf-nets enriched with static places, that model global resources. In this paper we prove the undecidability of soundness for rcwf-nets when there may be several static places and in which instances are allowed to terminate having created or consumed resources. In order to have a clearer presentation of the proof, we define an asynchronous version of a class of Petri nets with dynamic name creation. Then, we prove that reachability is undecidable for them, and reduce it to dynamic soundness in rcwf-nets. Finally, we prove that if we restrict our class of rcwf-nets, assuming in particular that a single instance is sound when it is given infinitely many global resources, then dynamic soundness is decidable by reducing it to the home space problem in P/T nets for a linear set of markings.

Bisimulation semantics are a very pleasant way to define the semantics of systems, mainly because the simplicity of their definitions and their nice coalgebraic properties. However, they also have some disadvantages: they are based on a sequential operational semantics defined by means of an ordinary transition system, and in order to be bisimilar two systems have to be "too similar". In this work we will present several natural proposals to define weaker bisimulation semantics that we think properly capture the desired behaviour of distributed systems. The main virtue of all these semantics is that they are real bisimulation semantics, thus inheriting most of the good properties of bisimulation semantics. This is so because they can be defined as particular instances of Jacobs and Hughes' categorical definition of simulation, which they have already proved to satisfy all those properties.

Several years before the popularization of the Internet, Mark Weiser proposed the concept of ubiquitous computing with the purpose of enhancing the use of computers by making many computers available throughout the physical environment, but making them effectively invisible to the user. Nowadays, such idea affects all areas of computing science, including both hardware and software. In this paper, a formal model for ubiquitous systems based on Petri nets is introduced and motivated with examples and applications. This simple model allows the definition of two-level ubiquitous systems, composed of a collection of processor nets providing services, and a collection of process nets requesting those services. The modeled systems abstract from middleware details, such as service discovery protocols, and security infrastructures, such as PKI’s or trust policies, but not from mobility or component compatibility.

In recent papers we have introduced Mobile Synchronizing Petri Nets, a new model for mobility based on coloured Petri Nets. It allows the description of systems composed of a collection of (possibly mobile) hardware devices and mobile agents, both modelled in a homogenous way and abstracting from middleware details. Our basic model introduced a colour to describe localities, but still lacked appropriate primitives to deal with security, and in fact it was equivalent to P/T nets. Then, we introduced the primitives to cope with security: a new colour for identifiers, basically corresponding to the natural numbers, that are created by means of a special transition. This mechanism allows us to deal with authentication issues. In this paper we discuss the expressiveness of the extended model with the authentication primitives. More specifically, we study several instances of the classical reachability and coverability problems. Finally, we also study a more abstract version of the mechanism to create identifiers, using abstract names, close to those in the π-calculus or the Ambient Calculus. We have proved that both models are strictly in between P/T nets and Turing machines.

The term Ubiquitous Computing was coined by Mark Weiser almost two decades ago. Despite all the time that has passed since Weiser's vision, ubiquitous computing still has a long way ahead to become a pervasive reality. One of the reasons for this may be the lack of widely accepted formal models capable of capturing and analyzing the complexity of the new paradigm. We propose a simple Petri Net based model to study some of its main characteristics. We model both devices and software components as a special kind of coloured Petri Nets, located in locations, that can move to other locations and synchronize with other co-located nets, offering and requesting services. We obtain an amenable model for ubiquitous computing, due to its graphical representation. We present our proposal in a progressive way, first presenting a basic model where coordination is formalized by the synchronized firing of pairs of compatible transitions that offer and request a specific service, and ad hoc networks are modeled by constraining mobility by the dynamic acquisition of locality names. Next, we introduce a mechanism for the treatment of robust security properties, namely the generation of fresh private names, to be used for authentication properties.

Maude has revealed itself as a powerful tool for implementing different kinds of semantics so that quick prototypes are available for trying examples and proving properties. In this paper we show how to define in Maude two semantics for Cardelli and Gordon's Ambient Calculus. The first one is the operational (reduction) semantics which requires the definition of Maude strategies in order to avoid infinite loops. The second one is a type system defined by Cardelli and Gordon to avoid communication errors. The correctness of that system was not formally proved. We enrich the operational semantics with error rules and prove that well-typed processes do not produce such errors. The type system is highly non-deterministic. We show here one possible way of implementing such non-determinism in the rules.