Roberto Vigo

Hanne Flemming Nielson

Riis Nielson

Hanne Riis Nielson

Uniform Protection for Multi-exposed Targets

Keywords: Security verification, distributed systems, protection analysis, security cost, Quality Calculus, Satisfiability Modulo Theories

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Common sense tells that classified information has to be protected according to its value. This simple principle is at the heart of the concept of multi-level security and the basis for developing access control policies [START_REF] Amoroso | Fundamentals of Computer Security Technology[END_REF]. Nonetheless, despite its simplicity, this design criterion is often ignored in the realisation of complex systems, whether they be software, physical, or cyber-physical systems. On the one hand, code complexity and composition may inadvertently give rise to various paths leading to expose the very same piece of information; on the other hand, usability best practices may prescribe, and technological constraints may oblige, to offer multiple ways to access the same information. The question whether uniform security checks are performed on paths leading to the same resource is then crucial, and its answer far from being obvious. The Quality Calculus has been introduced in [START_REF] Nielson | A Calculus for Quality[END_REF] for attacking the problem of Denial-of-Service resorting to default data whenever actual data cannot be obtained due to unreliable communication. More in general, the calculus offers an elegant framework for reasoning about systems where the same functionality can be triggered in multiple ways, and thus enjoy a branching control flow. Taking a process algebraic point of view, suitable for describing software systems but also organisations or physical infrastructure, we develop a static analysis on a value-passing version of the calculus to attack the questions highlighted above.

Given a system P and a location l of interest, the protection analysis computes the information an adversary needs in order to drive P to l, considering all possible paths. This is achieved by translating P into a set of propositional formulae describing the dependency between information and reachability of locations: each satisfying assignment of such set of formulae describes a way in which l can be attained. Moreover, associating costs to literals of such formulae, different assignments can be ranked so as to compute the minimal cost for reaching l. In particular, we consider an attacker model where adversaries are lucky: initially having no knowledge, they can decide to guess some information on their way to l, incurring the corresponding cost. Literals represent the knowledge of communication channels by the adversary. This approach proves useful as channels are abstract and flexible entities, which can model a great many cyber and physical scenarios. In particular, we assume that channels provide given degrees of security [START_REF] Mödersheim | Secure Pseudonymous Channels[END_REF], and quantify their strength: in the cyber world, a secure channel is implemented by means of cryptography, the cost of guessing it being a function of some cryptographic keys (e.g. number of bits for some cryptosystems); in the physical world, a channel may represent a door, its cost quantifying the effort needed to open it (e.g. grams of dynamite). While the correctness of such channels is investigated in the realm of protocol verification, any system with a substantial need for security is likely to have standardised mechanisms to achieve various degrees of protection, and modelling them with secure channels is a coarse yet reasonable abstraction. The ultimate goal of the framework is to check whether the protection ensured by the implementation, that is, the cheapest way for reaching l, is matching the specification requirements, formalised as a map from locations to desired confidentiality levels. The novelty of the protection analysis is two-fold: first, the problem of quantifying security checks and comparing desired with actual protection is interesting per se; second, the quest for optimal attacks relies on arbitrary cost structures and objective functions, and is implemented via a reduction to Satisfiability Modulo Theories (SMT) that can be exploited in a great many different contexts. Whilst our SMT approach to optimisation is not entirely novel, non-linearly ordered and symbolic cost structures have not been explicitly addressed so far in connection to this technique. The usefulness of the framework is demonstrated on the study of password recovery systems. We consider the Microsoft account system, where a challenge is sent to a previously registered e-mail or phone number, and the Yahoo!Mail system, which allows resetting a password upon answering previously selected questions. The results we present are obtained through an implementation of the analysis available at www.imm.dtu.dk/~rvig/quality-tool.html.

Outline. Section 2 introduces a motivating example developed throughout the paper. The calculus used to specify the example is presented in Sect. 3. In Sect. 4 the protection analysis is developed. The solution technique based on SMT is discussed in Sect. 5, where we also argue on the importance of complex cost sets. Section 6 concludes and sketches a line for future developments.

Related work. Our work is inspired by a successful strand of literature in protocol verification, where a protocol is translated into a set of first-order Horn clauses and resolution-based theorem proving is used to establish security properties [START_REF] Paulson | The inductive approach to verifying cryptographic protocols[END_REF][START_REF] Weidenbach | Towards an automatic analysis of security protocols in first-order logic[END_REF], and by the flow logic approach to static analysis [START_REF] Nielson | Flow Logic : A Multi-paradigmatic Approach[END_REF]. In particular, the translation from processes to propositional formulae is inspired by ProVerif [START_REF] Blanchet | Automatic verification of correspondences for security protocols[END_REF] translation of protocols into first-order Horn clauses, but can be more formally understood as a flow logic where the carrier logic is not the usual Alternationfree Least Fixed Point Logic, since it cannot express optimisation problems. In order to formalise the "need for protection" of a location we resort to confidentiality lattices, that are widely used for describing levels of security in access control policies. An excellent introductory reference is [1, chps. 6,7]. As for the solution technique we exploit, SMT is surveyed in [START_REF] De Moura | Satisfiability modulo theories: introduction and applications[END_REF], while [START_REF] Nieuwenhuis | On SAT Modulo Theories and Optimization Problems[END_REF][START_REF] Cimatti | Satisfiability Modulo the Theory of Costs: Foundations and Applications[END_REF] present two different approaches to solve optimisation problems via SMT. In particular, Nieuwenhuis and Oliveras [START_REF] Nieuwenhuis | On SAT Modulo Theories and Optimization Problems[END_REF] proposed to modify the DPLL(T ) procedure inherent to SMT solvers so as to look for optimal assignments, while Cimatti et al. [START_REF] Cimatti | Satisfiability Modulo the Theory of Costs: Foundations and Applications[END_REF] developed the search for an optimal assignments on top of an SMT solver, as we do in Sect. 5. Nonetheless, both these works focus on numeric weights, which in our settings are represented with linearly ordered cost structures. Our more general notion of weight is modelled after Meadow's cost sets, formalised as monoids in [START_REF] Meadows | A cost-based framework for analysis of denial of service in networks[END_REF]. Finally, another perspective on the technical developments underpinning the analysis points to computing prime implicants of a given formula [START_REF] Dillig | Minimum Satisfying Assignments for SMT[END_REF], where in our case primality is sought with respect to the cost set.

Motivating Example

We demonstrate the flexibility and usefulness of the framework on the problem of password recovery. As defined in the Common Weakness Enumeration [START_REF]Common Weakness Enumeration. Weak Password Recovery Mechanism for Forgotten Password[END_REF], "it is common for an application to have a mechanism that provides a means for a user to gain access to their account in the event they forget their password". It is then crucial to ensure that the protection to the account offered by the recovery mechanism is comparable to the protection provided by the password, otherwise we would have two paths leading to the same resource but performing a different amount of security checks. As noted by the Open Web Application Security Project [START_REF]Open Web Application Security Project: Choosing and Using Security Questions Cheat Sheet[END_REF]: "Weak password recovery processes allow stronger password authentication schemes to be bypassed. Non-existent password recovery processes are expensive to support or result in denial-of-service conditions." Below we encode such a system in the Value-Passing Quality Calculus.

System (νaccess) (νok) (νpwd) (!(Login|Recover))

Login  & ∀ (id?x id , pwd?x p ).  access!ok Recover  & ∀ (id?x id , & ∃ (mail?x m , pin?x c )).

4 case x m of some(y m ) :  pwd!ok else 6 case x c of some(y c ) :  pwd!ok else 0

Process System is modelled after Microsoft account login mechanism, in charge of granting access to services such as mailboxes and technical forums. The main process is composed by two parallel sub-processes, running an unbounded number of times: the first one models the normal login procedure, while the second one abstracts the password recovery mechanisms.

According to process Login, in order to be granted access a user has to provide their own id and the corresponding password. This is mimicked by the two inputs expected by the quality binder at label , which are simultaneously active.

The quality guard ∀ prescribes that both inputs have to be satisfied before proceeding, in any order. These inputs simulate two security checks: a party willing to authenticate into the system has to possess proper credentials, i.e., being able to communicate over id, pwd, and thus know such channels.

In the event the user forgot their password, the recovery mechanism comes into play. Microsoft offers two ways to recover a lost password: (i) a reset link is sent to an e-mail address previously registered by the user, or (ii) a 7-digit pin is sent to a phone number previously registered by the user. This behaviour is modelled by the quality binder at label  in process Recover. The binder is consumed as soon as the user has provided a valid id (e.g., an Outlook.com e-mail address), and proven their identity either through option (i) or option (ii). In the first case, the user needs to access a mailbox, simulated by an input on channel mail, while in the second case he or she has to provide the correct pin: the alternative is implemented by the existential guard ∃ instrumenting the inner quality binder.

The case clauses at labels ,  determine what combination of inputs triggered passing the binder. In both cases, the user gets a valid password for the account in question, simulated by the outputs at label  and , and hence will be able to fulfil the check enforced by process Login.

The key point of the example is that no matter how strong a user's password is, an attacker can always try to guess a 7-digit sequence 1 . In particular, the requirement for a password is having at least 8 characters and containing different cases, numbers, or symbols, which (almost) automatically makes a password stronger than the pin! In terms of confidentiality levels, this suggests that the desired security architecture is not necessarily met, as the protection offered by the three paths leading to authenticating, i.e. to label , might not be uniform, depending on the cost notion we resort to. While in this simple case such conclusion can be drawn after careful investigation of the system, there is a general need to develop automated techniques to cope with more complex scenarios. In the remainder of the paper we shall see how the protection analysis confirms our informal reasoning.

In the following, we discuss the syntax and the intended semantics of the process calculus we use as specification language. It encodes a value-passing fragment of the Quality Calculus, from which in particular we inherit quality binders and the distinction between data and optional data, that allow modelling robust systems and give rise to branching control flows. As far as this paper is concerned, however, the reader can think of the calculus as a broadcast π-calculus enriched with quality binders. Such construct enhances succinctness, thus easing the task of specifying complex systems, but does not increase the expressiveness, hence the developments carry seamlessly to a variety of process calculi.

The formal semantics of the calculus is briefly commented upon in Appendix A, for it is instrumental to formulate the correctness statements but does not constitute a novelty per se.

Syntax and intended semantics. The Value-Passing Quality Calculus is displayed in Table 1. The calculus consists of four syntactic categories: processes P , input binders b, terms t, and expressions e. A process can be prefixed by a restriction, an input binder, an output c!t of term t on channel c, or be the terminated process 0, the parallel composition of two processes, a replicated process, or a case clause. An output c!t broadcasts t to all processes ready to input over channel c; if there exists no such process, the output is consumed anyway (i.e., broadcasts are non-blocking actions). An input binder can either be a simple input c?x on channel c, or a quality binder & q (b 1 , . . . , b n ), which is consumed as soon as enough sub-binders have been satisfied, as dictated by the quality guard q. A quality guard can be any Boolean predicate: we use the abbreviations ∀ and ∃ for the predicates specifying that all the sub-binders or at least one sub-binder have to be satisfied before proceeding, respectively, as we have seen in the example. When a quality binder is consumed, some input variables occurring in its subbinders might have not been bound to any value, if this is allowed by the quality guard. In order to record which inputs have been received and which have not, we always bind an input variable x to an expression e, which is some(c) if c is the name received by the input binding x, or none if the input is not received but we are continuing anyway. In this sense, we say that expressions represent optional data, while terms represent data, in the wake of programming languages like Standard ML. In order to insist on this distinction, variables x are used to mark places where expressions are expected, whereas variables y stand for terms. The case clause in the syntax of processes is then used to inspect whether or not an input variable, bound to an expression, is indeed carrying data. The process case x of some(y) : P 1 else P 2 evolves into P 1 if x is bound to some(c), and in P 1 y is replaced by c; otherwise, if x is bound to none, P 2 is executed.

Observe that the adversary can always move into the scope of a restricted name by paying the corresponding cost, e.g. guessing pwd in the example. The standard semantics of restriction, according to which a new name c is only known within Table 1. The syntax of the Value-Passing Quality Calculus.

P ::= 0 | (νc) P | P1 | P2 | l b.P | l c!t.P | !P | l case x of some(y) : P1 else P2 b ::= c?x | &q(b1, • • • , bn) t ::= c | y e ::= x | some(t) | none
its scope, is encompassed by assigning c an infinite cost.

As usual, in the following we consider closed processes (no free variable), and we make the simplifying assumption that processes are renamed apart so that names and variables are bound exactly once. Table 1 defines a proper fragment of the original calculus, as it is not possible to check what is received by a given input. This simplification matches the spirit of the analysis, where the knowledge of channels corresponds to the capability of fulfilling the security checks that they represent.

Confidentiality labels. As argued in Sect. 1, different points in a system have to be protected according to the value of the information they process. This idea can be formalised introducing a simple, non-functional extension to the calculus, where a program point of interest is instrumented with a unique label l ∈ L. This is the case of input binders, outputs, and case clauses in Table 1: we limit labels to be placed before these constructs since they represent proper actions. In the following, we will denote labels with the numerals , , . . . , thus taking L = N.

We say that a label l is reached in an actual execution when the sub-process following l is ready to execute. Moreover, we assume to have a confidentiality lattice (Σ = {σ 1 , . . . , σ n }, Σ ), with greatest lower bound operator Σ , and a function γ : L → Σ that maps labels into confidentiality levels. In particular, γ(l 1 ) Σ γ(l 2 ) denotes that the confidentiality (i.e., need for protection) of the program point indicated by l 2 is greater than or equal to the confidentiality of the program point indicated by l 1 .

As an example of confidentiality lattice, consider the military lattice given by Σ = {unclassified, confidential, secret, top-secret}, with the ordering unclassified Σ confidential Σ secret Σ top-secret. More complex lattices, in particular non-linearly-ordered ones, are discussed in [1, chp. 7]. In our running example the intended security architecture prescribes γ(2) = γ(5) = γ(7), as these three program points have the effect of authenticating a user into the system. We can thus rely on a simple security lattice unrestricted Σ restricted, where the higher element is assigned to labels , , .

Protection Analysis

Given a process P , the protection analysis aims at estimating the amount of knowledge that a process Q has to possess in order for the execution of P |Q to reach a given location l in P . Intuitively, P is running and communicating in a hostile environment, and Q represents an adversary that aims at reaching a protected location, for example authenticating into the system. We focus on formalisations of P such that l is not reached unless some interactions with the environment take place: the running example of Sect. 2 does not specify the user who is supposed to be logging in, so as to rule out the legal way to authenticating and focus on malicious behaviours. We consider systems in which the communication takes place over secure channels, where the knowledge of a channel entails the capability of fulfilling the security checks governing the communication. The knowledge that an attacker Q needs to interact with P is thus defined as a set of such channels. Moreover, we can quantify this information by assigning costs to channels: in the case of IT systems, for instance, the degree of security provided by a channel is related to the strength of the cryptographic mechanisms it exploits, and in some cryptosystems be determined as the size of the cryptographic keys needed to communicate over the channel. Let Names be the set of channels occurring in P . We assume to have a function cost : Names → K that associates a cost k ∈ K to a channel c. Formally, we require (K, ⊕) to be a monoid equipped with a partial order K , such that (K, K ) is a lattice. Intuitively, the greater the protection a channel c ensures, the greater the effort required by Q in order to get access to the channel, and therefore the greater will be the value of cost(c) with respect to K . In the following, we will refer to K as the cost set of the analysis. We require ⊕ to be extensive, that is, the sum of two elements always dominates both the summands:

∀k 1 , k 2 ∈ K . k 1 K (k 1 ⊕ k 2 ) ∧ k 2 K (k 1 ⊕ k 2 ) (1)
Moreover, we assume that ⊕ is monotone and the least element ⊥ ∈ K is its identity element, that is, ⊕ is an upper bound operator of the lattice (K, K ), and therefore satisfies [START_REF] Amoroso | Fundamentals of Computer Security Technology[END_REF]. As highlighted by Meadows [START_REF] Meadows | A cost-based framework for analysis of denial of service in networks[END_REF], the monoid might not be commutative, as the order in which costs are paid might influence their combination. Whilst keeping this elegant generalisation, nonetheless we do not provide in practice any mechanism for re-determining costs dynamically, as the process is evaluated, nor do we discuss a context-sensitive notion of cost. The outcome of the analysis is a map δ : L → P(P(Names)) from labels to sets of sets of names (channels), an element {c 1 , . . . , c n } ∈ δ(l) denoting a set of channels whose total cost under-approximates the cost that Q incurs in order to enforce reaching l. Finally, δ(l) is computed such that all its elements have minimal costs with respect to the cost set. An element of δ(l) is related to the confidentiality lattice Σ = {σ 1 , . . . , σ n } by means of a function α : P(Names) → Σ, compressing cost regions into confidentiality levels:

α({c 1 , . . . , c n }) =        σ 1 if n i=1 cost(c i ) ∈ {k 1 1 , . . . , k h1 1 } . . . σ m if n i=1 cost(c i ) ∈ {k 1 m , . . . , k hm m }
where α is a well-defined function if the sets of costs {k 1 i , . . . , k hi i } are pairwise disjoint and their union is K. Moreover, it is natural to require that α is monotone. A simple example in the cost set (Z, +) is given by the choice

α({c 1 , . . . , c n }) =      low if n i=1 cost(c i ) ≤ 1024 medium if 1024 < n i=1 cost(c i ) ≤ 2048 high if 2048 < n i=1 cost(c i )
where numbers could represent the length of cryptographic keys, and we state for instance that a program point is poorly protected if no more than 1024 bits are necessary to attain it (for a fixed cryptosystem).

Intuitively, the function γ is the specification expressing the target security architecture of a system with respect to a given confidentiality lattice, while the function δ captures (an under-approximation of) how this architecture has been realised in the implementation. The overall aim of the analysis, i.e., checking whether the deployed protection lives up to the required confidentiality, can thus be expressed by the property

∀l ∈ L . γ(l) Σ Σ C∈δ(l) α(C)
A violation of this condition is referred to as a potential inversion of protection.

From processes to knowledge constraints

The recursive function [[P ]]tt, defined in Table 2, translates a process P into a set of constraints of the form ϕ p, where ϕ is a propositional formula and p a positive literal. The intended semantics of a constraint implements a backward style of reasoning, according to which if Q knows p, i.e., p = tt, then it must be because it knows (enough information to satisfy) ϕ. As we shall see below, the consequent ϕ accounts for the checks made on the path leading to disclosing p, namely input binders and case clauses. The antecedent p can either stand for a channel c, meaning that Q knows c, an input variable x, meaning that the related input is satisfied (i.e., x = some(c)), or a label l, meaning that l is attained. At each step of the evaluation, the first parameter of [[•]]• corresponds to the sub-process of P that has still to be translated, while the second parameter is a logic formula, intuitively carrying the hypothesis on the knowledge Q needs to attain the current point in P . The translation function is structurally defined over processes as explained below. If P is 0, then there is no location to be attained and thus no constraint is produced. If P = !P or P = (νc) P , then it spontaneously evolves to P , hence Q does not need any knowledge to attain P and gains no knowledge since no communication is performed. A parallel composition is translated taking the union of the sets into which the components are translated. Communication actions have instead an impact on the knowledge of Q: inputs represent checks that require knowledge, outputs fulfil those checks, and case clauses determine the flow of control. Whenever such an action [[ l a.P ]]ϕ is reached in the translation, a constraint ϕ l is generated: if the attacker Table 2. The translation from processes to propositional constraints.

[[0]]ϕ = ∅ [[!P ]]ϕ = [[P ]]ϕ [[P1|P2]]ϕ = [[P1]]ϕ ∪ [[P2]]ϕ [[(νc) P ]]ϕ = [[P ]]ϕ [[ l b.P ]]ϕ = [[P ]](ϕ ∧ hp(b)) ∪ th(ϕ, b) ∪ {ϕ l} [[ l c!t.P ]]ϕ = [[P ]]ϕ ∪ {ϕ c} ∪ {ϕ l} [[ l case x of some(y) : P1 else P2]]ϕ = [[P1]](ϕ ∧ x) ∪ [[P2]](ϕ ∧ ¬x) ∪ {ϕ l} hp(c?x) = c th(ϕ, c?x) = {(ϕ ∧ c) x}
hp(&q(c1?x1, . . . , cn?xn)) = [{q}](c1, . . . , cn)

th(ϕ, &q(b1, . . . , bn)) = n i=1 th(ϕ, bi)

[{∀}](h1, . . . , hn) = n i=1 hi

[{∃}](h1, . . . , hn) = n i=1 hi attains l, then the security checks on a path to l must be fulfilled, and thus ϕ must evaluate to tt. Moreover, the nature of action a determines whether or not other constraints are produced and how the translation proceeds. Consider a simple input l c?x.P : whenever such action is consumed, it must be that the attacker knows the communication channel c, therefore we translate P under the hypothesis ϕ ∧ c. Moreover, if the input is consumed, then x must be bound to some(c ), hence we produce a constraint (ϕ ∧ c)

x. These two steps respectively accommodate the hypothesis we need for passing a binder, and the thesis we can establish whenever a binder is passed. In Table 2 functions hp and th take care of formalising this intuition, that seamlessly applies to quality binders, where the hypothesis is augmented accounting for the combinations of inputs that satisfy the binder, as dictated by the quality guard q. The last section of Table 2 shows two cases for q, but any Boolean predicate can be used. The execution of an output l c!t satisfies all the security checks represented by inputs waiting on c. Therefore, if Q can trigger such output, it obtains the knowledge related to c without having to know the channel directly, and thus a constraint ϕ c is generated. It is worthwhile observing that this behaviour is justified by the broadcast semantics, and by the fact that the calculus is limited to testing whether or not something has been received over a given channel, shifting the semantic load on the notion of secure channel. Moreover, note that the asymmetry between input and output is due to the fact that outputs are non-blocking. A case construct is translated by taking the union of the constraints into which the two branches are translated: as the check is governed by the content of the case variable x, we record that the then branch is followed only when x is bound to some(c) by adding a literal x to the hypothesis, as we do for inputs, and we add ¬x if the else branch is followed. The set of constraints [[P ]]tt computed according to Table 2 can be normalised so as to produce a compact representation of system P . Whenever two rules ϕ p and ϕ p are in [[P ]]tt, they are replaced with a single rule (ϕ ∨ ϕ ) p. This simplification is intuitively sound since if ϕ leads to obtain p and ϕ leads to obtain p, then p is available to the attacker under the condition that ϕ ∨ ϕ is known. In the following, we assume to deal with sets of constraints in such format.

Attacker model: lucky attackers and insiders

A rule ϕ p in [[P ]

]tt describes how Q can attain p playing according to the rules of the system, namely fulfilling the checks described by ϕ. Nonetheless, when p is a channel, an attacker can always try to obtain it directly, for instance guessing some cryptographic keys. In order to account for this possibility, we enrich each rule ϕ c by replacing the consequent with the disjunction g c ∨ ϕ, where literal g c (for "guess c") represents the possibility of learning c directly, incurring the corresponding cost. Finally, for each channel c such that no rule ϕ c is in [[P ]]tt, we add to [[P ]]tt a constraint g c c, expressing that Q has no option but guessing the channel. It is worthwhile observing how resorting to propositional logic integrates with the under-approximating nature of the analysis: a channel can either be learnt or not, and its cost contribute or not to the cost of an attack. This means that we do not keep track of the number of attempts made to guess some information, and always assume that guessing c is successful whenever g c is found to be true. When looking for optimal combinations of channels with respect to the cost structure, we will then count the cost of those channels that Q must guess in order to attain the label of interest, thus obtaining an under-approximation of the cost of running the attack. Finally, notice how the cost map allows modelling insiders: by decreasing the cost of guessing a given piece of information we can model an attacker who has access to part of the secret, for instance to the rules according to which a random password is generated or to its first letter.

Example. The translation of our example returns a set containing the following constraints, augmented as explained above:

 id x id pwd x p id ∧ pwd  g access ∨ (id ∧ pwd) access g id id  id x id mail x m pin x c id ∧ (mail ∨ pin) ϕ  ϕ ∧ x m  g mail mail ϕ ∧ ¬x m  g pin pin ϕ ∧ (¬x m ) ∧ x c  g pwd ∨ (ϕ ∧ x m ) ∨ (ϕ ∧ (¬x m ) ∧ x c ) pwd
where the only way for Q to know id, mail, pin is to guess them. Observe that the capability of using the password channel is obtained either by satisfying the recovery mechanism or by guessing pwd. For the sake of conciseness, we have omitted the conjunct tt in all the constraints.

In order to compute the set of sets of channels δ(l) that allow reaching l incurring minimal costs, we need to solve an optimisation problem subject to the Boolean constraints [[P ]]tt, where can be freely interpreted as the propositional backward implication ⇐. There exist various techniques to cope with such problems, each suitable for particular choices of cost sets and objective functions. In the following, we show how to exploit an SMT solver to tackle the problem in its most general form. We limit to mention here that Pseudo-Boolean optimisation or Answer Set Programming with weighted rules are efficient and elegant alternatives for dealing with the monoid (Z, +) and linear objective functions.

The problem. In a nutshell, our task reduces to compute a satisfying assignment M of the propositional formula

ψ = l ∧ (ϕ p)∈[[P ]]tt (ϕ ⇐ p)
namely, we assume that l is reached and we look for the consequences (i.e., implicants of l). In particular, we are interested in all the assignments M that satisfy ψ, denoted M |= ψ, and are minimal with respect to a function of the literals g i 's representing the need for guessing channels:

f (g 1 , . . . , g n ) = (g 1 • cost(c 1 )) ⊕ • • • ⊕ (g n • cost(c n ))
where the cost of obtaining a channel contributes to the total cost of the attack only if Q decides to guess the channel, incurring the corresponding cost, g•cost(c) standing for if g then cost(c) else ⊥ (recall that ⊕ is assumed to be monotone and ⊥ its neutral element). If no solution is found, i.e. ψ is unsatisfiable, then the program point indicated by l is not reachable. Denoting M a satisfying assignment of ψ, we write δ(M ) for the set of literals that are true in M . Eventually, it might be that there exists a number of assignments with minimal costs, and thus δ(l) is defined as

δ(l) = {δ(M ) | M |= ψ ∧ minimal(M )}
and finally we shall take as result of the analysis the security level σ minimal among those onto which α maps the sets of channels in δ(l), or their greatest lower bound in case they are incomparable (recall that Σ is a lattice).

An SMT-based algorithm. Such an optimisation problem can be tackled by computing assignments for a list π 1 , . . . , π n of SMT problems, where π i is a more constrained version of π i-1 that requires to improve on the cost of the current solution. The initial problem π consists of the propositional constraints ψ and of the objective function f , whose value is stored in variable goal. Then, while the problem is satisfiable, we improve on the cost of the current assignment by asserting new constraints which tighten the value of goal, until unsatisfiability is Data: The problem π ≡ ψ ∧ (goal := f (g1, . . . , gn)) Result: the set M of pairs (assignment,cost) such that the assignment is minimal w

.r.t. f M ← ∅; while π satisfiable do M ← get-model(π); k ← M (goal); forall (M , k ) ∈ M | k K k do // M outperforms M M ← M \ {(M , k )} end M ← M ∪ {(M, k)}; π ← π ∧ ¬( n i=1 (ci = M (ci))) ∧ ¬(goal K k); end Algorithm 1:
The SMT-based solving procedure. reported. As for the cost set (comparing and combining costs), SMT solvers offer native support for numeric costs and common mathematical functions, while more complex cost sets have to be encoded manually. Algorithm 1 displays the pseudo-code of the procedure. In particular, observe that when a new problem π i is generated, additional constraints are asserted that ask for (i) a different assignment and (ii) a non-greater cost: the former condition speeds up the search, while the latter explores the cost frontier. The termination of the algorithm is ensured by the finiteness of possible assignments to the propositional variables of the π i 's, whose propositional structure does not change throughout the loop, and by the fact that the same assignment cannot occur twice as solution due to the new constraints we generate in each iteration: at most, we need to solve as many π i 's as models of ψ (ALL-SAT). The correctness of the procedure stems from the fact that when unsatisfiability is claimed, by construction of the π i 's there cannot exist further assignments that comply with the cost constraints. Finally, observe that the Boolean satisfiability problem is NP-complete, but in the last decade solvers have been developed that can handle instances with millions of variables, and are increasingly used in software verification. Our implementation is based on Microsoft Z3.

Example. Consider the login system discussed in Sect. 2, and assume to work in the cost set (Z, +). The engineering of a sensible cost map is a delicate task that involves cryptographic arguments. Due to space constraint we make here the simplistic assumption that costs to channels are given by the number of bits to be guessed: cost(pin) = 28 (7 digits, 4 bits each) and cost(pwd) = 56 (8 symbols, 7 bit per ASCII symbol). We assume that the user id is known (the target email itself, for instance), and that the password of the third-party mailbox is comparable to pwd (as the constraints put by Microsoft are customary also to other e-mail providers). Finally, we disregard channel access as it is only used after the label of interest is reached. The problem is thus to minimise f (g id , g pwd , g mail , g pin ) = g id •cost(id) + g pwd •cost(pwd) + g pin •cost(pin) + g mail •cost(mail) under the constraints given by ψ where label  is asserted. Instructed with such input, our procedure finds that the formula is satisfiable and the single cheapest assignment is M = [g id → tt, g pwd → ff, g mail → ff, g pin → tt], with cost given by cost(id) + cost(pin) = 28, and entailing δ() = {{id, pin}}. As for the desired security levels, we observed in Sect. 3 that γ() = γ() = γ() = restricted should hold, for we want the account to be equally protected on all the paths leading to granting access. As the cost for accessing an account in normal condition is 56, it is reasonable to set

α({c 1 , . . . , c n }) = restricted if n i=1 c i ≥ 56 unrestricted otherwise
We would like to verify that restricted Σ α({id, pin}), which is false since cost(id) + cost(pin) = 28. It is thus the case that the implementation potentially guarantees less protection than the amount required by the specification, and therefore we shall issue a warning to the designer of the system. Obviously, costs are central in determining the outcome of the analysis. For example, we could consider to choose pwd from a password dictionary, for it is unrealistic to assume randomly generated bits: the size of such dictionaries is usually less than the number of sequences of 7 digits, and thus with this cost map the analysis might say that the recovery mechanism offers enough protection. Likewise, a limit to the number of attempts can equalise the protection. Finally, it is worthwhile noticing that the framework can be exploited to measure the distance between the implementation and the specification, and not only there qualitative compliance.

Motivating complex cost sets

So far we have worked with an example in the cost set (Z, +), for it is natively encoded into SMT solvers and matches a first intuition of the notion of cost. More realistic numeric considerations can be formalised in the increasingly popular frameworks for the quantification of information leakage, e.g. [START_REF] Alvim | Measuring Information Leakage Using Generalized Gain Functions[END_REF], obtaining more robust definitions of function α. Nonetheless, it is not always the case that we are able to describe with numbers the security provided by channels: sometimes the techniques used to ensure security are even incomparable. Observe that Algorithm 1 is already equipped to cope with the more general problem of optimising on partially ordered cost sets. An interesting case of nonlinear cost sets is offered by the study of security in Cyber-Physical Systems, where components combine both software and physical features. In particular, in such systems an attack could require to assemble cyber actions with physical tampering [START_REF] Vigo | The Cyber-Physical Attacker[END_REF], whose costs can either be comparable or not depending on the nature of the quantities we are interested in (for instance, energy and memory are not directly comparable). In general, three elements characterise the problem and push for the comprehensive SMT-based approach: the non-linearity of the cost set, its symbolic nature, and the non-linearity of the objective function.

A mundane approach to password recovery. Yahoo!Mail password recovery mechanism differs from the one provided by Microsoft account in that it is (also) possible to recover a password by answering two personal questions like "What is your mother's maiden name?". It is unclear how to quantify the difficulty of such questions in terms of numbers. Nonetheless, it is simpler for an attacker to get hold of such secrets than guessing a randomly generated pin [START_REF] Griffith | Messin' with Texas Deriving Mother's Maiden Names Using Public Records[END_REF]. A symbolic quantification of the two paths leading to logging into the mailbox can then be modelled in the cost set ({cheap, expensive}, ⊕), where the cost of answering a question is cheap and the cost of guessing the password is expensive. As for the monoid operator, a suggestion is to use max(•, •), since asking one, two, or three questions will annoy an attacker but does not really make their task much harder. The SMT implementation of this example requires to encode the cost structure, that is, declaring its elements and defining the ordering relation as well as the monoid operator. Running the analysis in this cost set, we verified the existence of a cheap path leading to authenticating, namely the path that exploits the question-based recovery mechanism. The framework thus suggests that such option should not be allowed, otherwise we would not provide uniform security on all paths guarding the protected region.

Conclusion

In the design of software, physical, and cyber-physical systems, security is often perceived as a qualitative need, but can only be attained quantitatively. Especially when physical components are involved, it is simply impossible to predict and confront any possible attack. Even if it were possible, it would be unrealistic to have an unlimited budget to implement security mechanisms. The protection analysis we presented has both the merit of automatically inferring the attacks to which a system is subject, among those accountable for in the framework, and to estimate the effort required by a lucky attacker for bypassing the protection mechanisms in place. Hence, the approach enables to identify potential weak paths and compare desired with actual protection. Moreover, the framework allows reasoning with symbolic and non-linearly ordered cost structures, as it is often more natural and informative to describe the relationships between different protection mechanisms instead of assigning them absolute numbers. We showed how the analysis applies to real scenarios giving meaningful insights on the problem of password recovery. Finally, the SMT-based optimisation technique proposed for computing the analysis is exploitable in all the contexts where propositional models have to be ranked. Future developments include extending the approach beyond Boolean considerations about guessing capabilities, as they intuitively integrate with a probabilistic view of the world. On the practical side we aim at a stand-alone version of the SMT-based solution engine, so as to boost its applicability to other problems.

P ≡ P P1 ≡ P2 ⇒ P2 ≡ P1 P1 ≡ P2 ∧ P2 ≡ P3 ⇒ P1 ≡ P3 P | 0 ≡ P P1 | P2 ≡ P2 | P1 P1 | (P2 | P3) ≡ (P1 | P2) | P3 (νc) P ≡ P if c / ∈ fn(P ) (νc1) (νc2) P ≡ (νc2) (νc1) P (νc) (P1 | P2) ≡ ((νc) P1) | P2 if c / ∈ fn(P2) !P ≡ P |!P P1 ≡ P2 ⇒ C[P1] ≡ C[P2]
A Broadcast Semantics and Correctness Statements

The semantics of Table 4 is based on the transition relation P =⇒ P , which is enabled by combining a local transition λ ---→ with the structural congruence defined in Table 3. The semantics models asynchronous broadcast communication, and makes use of a label λ ::= τ | c 1 !c 2 to record whether or not a broadcast is available in the system. Output is thus a non-blocking action, and when it is performed the broadcast is recorded on the arrow. When a process guarded by a binder receives an output, the broadcast remains available to other processes willing to input. This behaviour is encoded in rules (In-ff) and (In-tt), where we distinguish the case in which a binder has not received enough input, and thus keeps waiting, from the case in which a binder is satisfied and thus the computation may proceed. These rules rely on two auxiliary relations, one defining how an output affects a binder, and one describing when a binder is satisfied (enough inputs have been received), displayed in the third and fourth section of Table 4, respectively, and originally introduced in [START_REF] Nielson | A Calculus for Quality[END_REF].

The semantics is instrumental to phrase the correctness of the analysis: if P |Q =⇒ * C[ l P ] then ∃C ∈ δ(l) s.t. C ⊆ fn(Q) i.e., for all the executions in which Q can drive P to l, the analysis provides a set of channels that under-approximates the knowledge required by Q. Technically, it seems convenient to organise a formal proof in two steps. First, if P |Q reaches l then P |H[fn(Q)] reaches l, where process H is the hardest attacker possible and is parametrised on the knowledge of Q. H can be thought as the (infinite) process executing all possible actions on fn(Q), and the proof simply argues that whatever Q can, H can (Lemma 1). A similar approach is explained in detail in [START_REF] Nielson | Validating firewalls using flow logics[END_REF]. Finally, the second step shows that if P |H[C ] reaches l, then there must be a set C ∈ δ(l) such that C ⊆ C (Theorem 1).

Definition 1 (

 1 Hardest attacker). Let N = {c 1 , . . . , c n } be a finite set of names. H[N ] is the process that does all possible sequence of output actions on N : H[N ] (νd) (!(c 1 !d)) | . . . | (!(c n !d)).

Table 4 .- 2 -c 1 !c 2 -c 1 !c 2 -c 1 !c 2 ---→ P 1 P1|P2c 1 !c 2 -Theorem 1 (

 421212121121 The transition rules of the calculus.P1 ≡ (ν -→ c ) P2 P2 λ --→ P 1 c1!c2 b → b b :: ff θ P1 | l b.P2 c 1 !c 2 ---→ P 1 | l b .P2 (In-ff) P1 --→ P 1 c1!c2 b → b b ::tt θ P1 | l b.P2 --→ P 1 | P2θ (In-tt) l case some(c) of some(y) : P1 else P2 τ ---→ P1[c/y] (Then)l case none of some(y) :P1 else P2 τ ---→ P2 (Else) P τ ---→ P (νc) P τ ---→ (νc) P (Res-tau) P c 1 !c 2 ---→ P (νc) P c 1 !c 2 ---→ (νc) P if c = c1 ∧ c = c2 (Res-out) --→ P 1 |P2 if P2 = !P 2 ∨ P2 = l c 1 !c 2 P 2 (Par-out) c1!c2 c1?x → [some(c2)/x] c1!c2 c3?x → c3?x if c1 = c3 c1!c2 b1 → b 1 • • • c1!c2 bn → b n c1!c2&q(b1, . . . , bn) → &q(b 1 , . . . , b n ) c?x :: ff [none/x] [some(c)/x] ::tt [some(c)/x] b1 ::v 1 θ1 • • • bn ::v n θn &q(b1, . . . , bn) ::v θn • • • θ1 [{q}](v1, . . . , vn) = v Lemma 1. Let P, Q be processes. If P |Q =⇒ * C[ l P ] then P |H[fn(Q)] =⇒ * C[ l P ]. Proof. By induction on the length of the derivation sequence. Lemma 2. Let P be a process and N a set of names. If P |H[N ] =⇒ * C[ l P ], then, for all processes R with R ≡ C[ l P ] and for all contexts C , P |H[N ] =⇒ * C [R ]. Proof. By induction on the shape of the inference tree for the step R ≡ C[ l P ]. Correctness of the protection analysis). Let P be a process and N a set of names. If P |H[N ] =⇒ * C[ l P ], then there exists N ∈ δ(l) such that N ⊆ N . Proof. By induction on the length of the derivation sequence, exploiting Lemma 2 in the inductive step.

Table 3 .

 3 The structural congruence of the calculus.

As of Oct.

there seemed to be no limit to the number of attempts one could try -we stopped our experiment at about 30. Some of our findings have been informally communicated in a number of situations and now we observe that they enforced both such limit and a daily threshold. While this mutation does make it more difficult to quantify the strength of the mechanism (cf. Sect. 5), it does not affect the relevance of the framework.

Acknowledgement. This work is supported by the IDEA4CPS project, granted by the Danish Research Foundations for Basic Research (DNRF86-10).


Stephan Mennicke
email: mennicke@ips.cs.tu-bs.de

Jens-Wolfhard Schicke

Ursula Goltz
email: goltz@ips.cs.tu-bs.de

On the Step Branching Time Closure of Free-Choice Petri Nets

Free-choice Petri nets constitute a non-trivial subclass of Petri nets, excelling in simplicity as well as in analyzability. Extensions of free-choice nets have been investigated and shown to be translatable back to interleaving-equivalent free-choice nets. In this paper, we investigate extensions of free-choice Petri nets up to step branching time equivalences. For extended free-choice nets, we achieve a generalization of the equivalence result by showing that an existing construction respects weak step bisimulation equivalence. The known translation for behavioral free-choice does not respect step branching time equivalences, which turns out to be a property inherent to all transformation functions from this net class into (extended) free-choice Petri nets. By analyzing the critical structures, we find two subsets of behavioral free-choice nets that are step branching time equivalent to free-choice nets. Finally, we provide a discussion concerning the actual closure of free-choice Petri nets up to step branching time equivalences.

Introduction

A well-known abstraction from distributed systems is the model of Petri nets, arranging the aspects of causally dependent and concurrent actions in a neat graphical representation. Petri nets stem from the ideas given in the PhD thesis of C. A. Petri [START_REF] Petri | Kommunikation mit Automaten[END_REF]. Petri forced system states to be structured by means of local states, meeting the concepts of distributed systems, where components are distributed over several locations. That actions of a single component depend on local state information only is naturally captured by the firing rule of Petri nets. In addition, Petri nets offer an intuitive notion of concurrent computation by the step firing rule, a generalization of the firing rule allowing more than one transition to fire in parallel (or unordered). Hence, system analysis of distributed systems specified by Petri nets may actually be aware of uncertainties in the order in which actions occur. Although decidable, many interesting properties such as liveness or boundedness of Petri nets are hard in terms of computational complexity [START_REF] Esparza | Decidability and complexity of petri net problems -an introduction[END_REF].

The Petri net class of free-choice Petri nets (FC-nets) is non-trivial w. r. t. expressive power, while efficient analysis algorithms are provided [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Esparza | Decidability and complexity of petri net problems -an introduction[END_REF]. The core Fig. 1: The two net principles allowed in FC-nets. idea of free-choice is that if the system sometimes has a choice between multiple actions, it always has this choice. It is never the case that only some of these actions are available. Choices between actions may be resolved independently of the system state. The simplest implementation in terms of a Petri net class is provided by FC-nets, comprising only those nets in which conflicting transitions have one condition at most. The two basic subnets following from this restriction are depicted in Fig. 1.

The fundamental results leading to efficient analysis algorithms of FC-nets are achieved in the field of structure theory [START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF], where semantic properties shall follow from syntactical ones. For instance, the Commoner/Hack Criterion for FC-nets implies liveness, reducing the liveness problem to a semi-structural property, the basis for efficient analysis. For a comprehensive overview on structure theory, we refer to Best and Wimmel [START_REF] Best | Structure theory of petri nets[END_REF]. Esparza provides a survey on computational complexity of analysis algorithms for (free-choice) Petri nets [START_REF] Esparza | Decidability and complexity of petri net problems -an introduction[END_REF].

E. Best states that most of the fundamental results from structure theory do not persist, when using a more expressive net class than FC-nets [START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF]. However, there are Petri net classes exhibiting the basic concept of free-choice to some degree, provoking the desire to relate them to the original FC-nets. Extended free-choice nets exhibit free-choice in that transitions sharing one precondition, share all preconditions. Once again, the set of transitions to choose from does not depend on the system state. In contrast to the aforementioned classes, freechoice may also be described by behavioral notions. A Petri net is a behavioral free-choice net if in any system state (reachable from the initial state), two conflicting transitions are either enabled or disabled. Hence, whenever the system has the choice of some of these transitions, it can choose between all of them, again independent of the system state. Best and Shields prove all these net classes equivalent by showing transformations from behavioral free-choice nets to extended free-choice nets and from extended free-choice nets to FC-nets to respect a form of interleaving simulation equivalence [START_REF] Best | Some equivalence results for free choice nets and simple nets and on the periodicity of live free choice nets[END_REF]. However, it is unclear whether the results from structure theory transfer from FC-nets to free-choice related net classes when considering step semantics of Petri net behavior. Such a transfer would help greatly in applying analysis algorithms for FC-nets to distributed systems where step semantics are relevant.

We analyze the class of FC-nets up to step branching time equivalences. The Linear Time -Branching Time Spectrum by van Glabbeek provides a lattice of equivalence notions for linear time behavior such as traces, and branching time behavior such as bisimulation [START_REF] Van Glabbeek | The linear time -branching time spectrum[END_REF]. We aim at covering the branching behavior of a system, i. e., we take the decision-making process into account. Failure equivalence is one of the weakest branching time equivalences, serving as a separator equivalence. If a transformation from one net class into another is impossible, we show that any transformation respecting at least failure equivalence must fail. On the contrary, we use bisimulation equivalence to prove that a particular transformation is correct. For Petri nets, there are two different approaches in interpreting the equivalence notions by van Glabbeek, (i) interleaving, i. e., one action at a time, and (ii) steps, i. e., independent actions may occur unordered or even in parallel. As distributed systems operate in an asynchronous fashion, the step interpretation is appropriate here. Transformations implementing a form of busy waiting protocol are not tolerated. Thus, we incorporate divergencesensitiveness in the equivalences.

Extended free-choice nets remain equivalent to FC-nets under step branching time equivalences. We generalize the proof by Best and Shields to concurrencyaware equivalences. Unfortunately, the well-known construction from behavioral free-choice nets to extended free-choice nets does not respect step branching time behavior, in general. This property turns out to be inherent to all transformation functions from behavioral to (extended) FC-nets. We tackle this problem by analyzing two subsets of behavioral free-choice nets, both being step branching time equivalent to FC-nets. Finally, we discuss the step branching time closure of FC-nets by symmetrically asynchronous Petri nets, a net class occurring in the literature discussion of the difference between synchronous and asynchronous behavior [START_REF] Van Glabbeek | On synchronous and asynchronous interaction in distributed systems[END_REF]. We prove that FC-nets and symmetrically asynchronous Petri nets are equivalent up to step branching time, linking the closure of the class of FC-nets to the closure of symmetrically asynchronous Petri nets.

In Sect. 2, we introduce the basic notions for this paper. The relation between FC-nets and extended free-choice nets is established in Sect. 3 whereas Sect. 4 discusses relations to behavioral free choice net classes. Sect. 5 discusses symmetrically asynchronous Petri nets and their relation to FC-nets. By Sect. 6, we conclude the paper.

Basic Notions

In this section, we provide basic notions necessary to follow the employed theories and results concerning free-choice Petri nets. The state notion of Petri nets is based on multisets, which are sets possibly containing the same element multiple times.

Definition 1 (Multiset). Let S, S be non-empty sets. A multiset M over S (M ∈ N S ) is a function M : S → N. For two multisets A and B over S, we define (i) A + B to be the multiset over S with (A + B)(s) = A(s) + B(s) for all s ∈ S, (ii) A-B to be the multiset over S with (A-B)(s) = max{0, A(s)-B(s)} for all s ∈ S, (iii) (A ∩ B) likewise via (A ∩ B)(s) = min{A(s), B(s)}, and (iv) A ≤ B iff A(s) ≤ B(s) for all s ∈ S. The operations (i)-(iii) are generalized to multisets A over S and B over S , resulting in a multiset (A op B) over S ∪ S .

By 0 S we denote the empty multiset over S. Let S ⊇ A = {a 1 , . . . , a n }. Then A denotes the multiset with A(a i ) = 1 (i = 1, . . . , n).

Petri Nets

In this paper, we consider finite labeled place/transition nets, consisting of two disjoint finite sets P and T , the set of places and the set of transitions, a flow relation F , relating places and transitions, an initial marking, i. e., a multiset over the set of places, and a labeling function for transitions.

Definition 2 (Petri Net). Let Act with τ ∈ Act be a finite set of actions. A Petri net is a 5-tuple N = (P, T, F, M 0 , l) where P and T are disjoint finite sets, F ⊆ (P × T ) ∪ (T × P ), M 0 a multiset over P , and l : T → Act ∪ {τ } a function. If l is injective and l(T ) ⊆ Act, then N is plain. If l is injective except for τ , i. e., ∀t, t ∈ T : t = t ∧ l(t) = l(t ) ⇒ l(t) = τ , then N is plain-labeled. For a node n ∈ P ∪ T , by • n := {x ∈ P ∪ T | (x, n) ∈ F } we denote the preset of n and, analogously, by n • := {y ∈ P ∪ T | (n, y) ∈ F } the postset of n. The notions for pre-and postset canonically extend to (multi-)sets of nodes.

We assume plain Petri nets as input models for the transformations we describe throughout the paper, because τ -transitions are reserved for implementation purposes. Transformed nets shall preserve the original net transitions but may make use of additional invisible ones. Thus, we expect transformed nets to be plain-labeled.

Petri nets offer a graphical notation, where places are drawn as circles, transitions as boxes, and the flow relation is represented by directed edges, called arcs. A marking M is graphically represented by drawing M (p) black dots in the center of each place p. Definition 3 (Firing Rule). Let N = (P, T, F, M 0 , l) be a Petri net, M, M ∈ N P , G ∈ N T , G non-empty and finite. G is called a step from M to M , denoted

M [G N M iff (i) G is enabled under M , denoted M [G N , meaning that • G ≤ M , and (ii) M = (M -• G) + G • . If N is clear from the context, we write M [G instead of M [G N (likewise for M [G N M ). A marking M is reachable in N = (P, T, F, M 0 , l) if there are mark- ings M 1 , . . . , M n and a sequence of steps G 1 , . . . , G n such that M i-1 [G i N M i (0 < i ≤ n) and M = M n .
The set of all reachable markings together with the step relation [G N induces the state graph of a Petri net, called reachability graph.

A common semantic requirement on Petri nets is that each place holds at most one token at each reachable marking. Such nets are called 1-safe nets. For finite Petri nets, this property implies that the reachability graph of a net is finite, thus exhibiting the expressive power of finite automata. For the generality of our results, we use a more expressive class of Petri nets, but maintain an important aspect of safe Petri nets: Two conflicting transitions, i. e., two transitions sharing a place in their preset, may not fire concurrently, i. e., in the same step. This class of nets is called structural conflict nets and was first introduced by van Glabeek et al. [START_REF] Van Glabbeek | Abstract processes of place/transition systems[END_REF].

Definition 4 (Reachable Markings, 1-safety, Structural Conflict Net).

Let N = (P, T, F, M 0 , l) be a Petri net. The set [N of reachable markings of N is defined as the smallest set containing M 0 , closed under

[G N , meaning that if M ∈ [N and M [G M for any G, then M ∈ [N . N is 1-safe iff M ∈ [N implies that for all p ∈ P : M (p) ≤ 1. The concurrency relation ⊆ T 2 is given by t u ⇔ ∃M ∈ [N : M [{t} + {u} N . N is a structural conflict net iff for all t, u ∈ T with t u we have • t ∩ • u = ∅.
For the remainder of this paper, we assume all nets to be structural conflict nets.

Semantic Equivalences

The comparison between classes of Petri nets may be performed either by structural equivalences or equivalences capturing certain aspects of the behavior of the net classes. We concentrate on behavioral equivalences in this paper. For a comprehensive overview on comparative equivalence notions, see, e. g., [START_REF] Van Glabbeek | The linear time -branching time spectrum[END_REF].

As a basis for the equivalence notions, we introduce three transition relations for visible and invisible steps, as well as a trace relation. To this end, we divide the set of transitions of a Petri net N into a set of observable transitions O(N Again, we drop the subscripted net identifier N when appropriate.

) := {t ∈ T | l(t) ∈ Act} and a set of invisble transitions U(N ) := {t ∈ T | l(t) = τ }. Definition 5 (Labeled Transition Relation). Let N = (P, T, F, M 0 , l) be a Petri net over Act. (i) M A -→ N M iff ∃G ∈ N O(N ) : M [G M ∧ l(G) = A, (ii) M τ -→ N M iff ∃t ∈ U(N ) : M [{t} M , and (iii) M σ =⇒ M iff σ = a 1 a 2 . . . a n ∈ Act * and M τ -→ * N {a1} -→ N τ -→ * N {a2} -→ N τ -→ * N . . .
Based on the previously defined transition relation, we are now able to define our step branching time equivalences. The first equivalence is step failure equivalence being the weakest step branching time equivalence we are aware of. It comprises the trace behavior together with a set of steps, the net is not capable of after a given trace. Definition 6 (Step Failure Equivalence). Let N = (P, T, F, M 0 , l) be a Petri net labeled over Act, σ ∈ Act * , and

X ⊆ N Act . (σ, X) is a step failure pair of N iff ∃M : M 0 σ =⇒ M ∧ M τ -→ ∧∀A ∈ X : M A -→ . F(N ) denotes the set of all step failure pairs of N . Two Petri nets N 1 , N 2 are step failure equivalent, N 1 ≈ F N 2 iff F(N 1 ) = F(N 2 ).
Note that we use a weak (abstracting from τ s) version here, as the equivalences we employ have to handle visible as well as invisible transitions. Furthermore, step failure equivalence is divergence-sensitive in that any form of divergence caused by τ -transitions results in exclusion of the corresponding trace from the set of failure pairs. This is ensured by the requirement that from the reachable marking M , no τ -transition may be enabled. We will use step failure equivalence to obtain separation results. Towards the other end of the step branching time spectrum, there is step bisimilarity. Again, we employ the weak version enabling us to abstract from τ -transitions.

Definition 7 (Weak Step Bisimilarity). Let N i = (P i , T i , F i , M i , l i ) (i = 1, 2) be two Petri nets. A weak step bisimulation between N 1 and N 2 is a relation R ⊆ N P1 × N P2 such that 1. (M 1 , M 2 ) ∈ R and 2. if (M 1 , M 2 ) ∈ R, then (a) M 1 τ -→ M 1 ⇒ ∃M 2 ∈ N P2 : M 2 τ -→ * M 2 ∧ (M 1 , M 2 ) ∈ R, (b) M 1 A -→ M 1 ⇒ ∃M 2 ∈ N P2 : M 2 τ -→ * A -→ τ -→ * M 2 ∧ (M 1 , M 2 ) ∈ R, (c) M 2 τ -→ M 2 ⇒ ∃M 1 ∈ N P1 : M 1 τ -→ * M 1 ∧ (M 1 , M 2 ) ∈ R, (d) M 2 A -→ M 2 ⇒ ∃M 1 ∈ N P1 : M 1 τ -→ * A -→ τ -→ * M 1 ∧ (M 1 , M 2 ) ∈ R.
N 1 and N 2 are weak step bisimilar, N 1 ≈ B N 2 iff there exists a weak step bisimulation between N 1 and N 2 .

If two nets are weak step bisimilar, then they are step failure equivalent. The converse does not hold, in general. Hence, step failure equivalence is coarser than weak step bisimulation thus N 1 ≈ F N 2 implies N 1 ≈ B N 2 . Therefore, we use step failure equivalence for separation results.

Free-Choice and Extended Free-Choice

Free-choice Petri nets (FC-nets) are generalizations of S-nets and T-nets, both representing net classes providing efficient analysis algorithms, e. g., for liveness or boundedness [START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF]. FC-nets allow choices between transitions, but only if there is at most one place in the preset of the conflicting transitions (cf. Fig. 1 (a)), and synchronization of places, but only in the way that there is at most one transition in the postset of the synchronized places (cf. Fig. 1 (b)). The conflict pattern refers to restrictions imposed on S-nets, while the synchronization pattern follows restrictions as imposed on T-nets. Hence, every time a conflict occurs, it occurs between the same set of transitions and it is not influenced by the rest of the net.

Definition 8 (Free-Choice Petri Net). A Petri net N = (P, T, F, M 0 , l) is a free-choice Petri net (FC-net) iff ∀p ∈ P ∀t ∈ T : (p, t) ∈ F ⇒ p • = {t} ∨ • t = {p}.
FC-nets come with a natural notion of distributed component, called free-choice cluster. Given an FC-net N = (P, T, F, M 0 , l), the free-choice cluster of a transition t ∈ T is the conflict cluster of t, i. e., [t] = ( • t) • . The set of all conflict clusters and thus free-choice clusters of N , denoted by C(N ), imposes a partitioning on the set of transitions if N is an FC-net. Thus, a free-choice cluster may be seen as a component of a system N . Note that each component has at most one role, either to resolve a conflict between actions or to synchronize As already motivated, FC-nets excel in a wide range of applications, mostly due to their structural properties implying semantic properties. For a comprehensive overview, we refer to [START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF][START_REF] Best | Structure theory of petri nets[END_REF]. Unfortunately, not every Petri net is an FC-net (cf. Fig. 2). However, if a Petri net is behavioral equivalent to an FC-net, analysis results on the transformed net enables us to (partially) reason about semantic properties of the original net. The Petri net depicted in Fig. 2 (b) belongs to the class of extended freechoice nets (EFC-nets). EFC-nets are characterized by the property that if two transitions share any place in their preset, then they share all preplaces. Thus, these nets exhibit the free-choice property to a certain extent, as conflicting transitions always depend on the same set of places.

Definition 9 (Extended Free-Choice Net). A Petri net N = (P, T, F, M 0 , l) is an extended free-choice net iff ∀t 1 , t 2 ∈ T :

• t 1 ∩ • t 2 = ∅ ⇒ • t 1 = • t 2 .
Furthermore, we observe that the clustering described for FC-net transitions also works in EFC-nets, i. e., C(N ) of an EFC-net N is a partition on the set of transitions of N . Therefore, we call a conflict cluster of an EFC-net EFCcluster. Note that every FC-net is also an EFC-net, but the converse does not hold in general. However, Best and Shields proved that there is a behavioral correspondence by showing that EFC-nets may be transformed into FC-nets, respecting a form of interleaving simulation [START_REF] Best | Some equivalence results for free choice nets and simple nets and on the periodicity of live free choice nets[END_REF].

The core idea of that transformation is to split an EFC-cluster C ∈ C(N ) into two operational parts, (i) a synchronization of all input places of C and (ii) a choice between all transitions in C. For (i), an unobservable transition is added, consuming one token from each input place of C and producing a token to an additional place p C . In part (ii), all the transitions in C consume from p C . An example transformation, namely from the EFC-net in Fig. 2 (b) into the corresponding FC-net is depicted in Fig. 3 (a). Formally, the transformation is defined as follows [START_REF] Best | Some equivalence results for free choice nets and simple nets and on the periodicity of live free choice nets[END_REF][START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF].

τ t u (a) t u v (b)
Fig. 3: FC-net and EFC-net Constructions.

Definition 10 (FC(N )). Let N = (P, T, F, M 0 , l) be a Petri net. We define FC(N ) := (P , T , F , M 0 , l ) where

P = P ∪ {p [u] | [u] ∈ C(N )} T = T ∪ {τ [u] | [u] ∈ C(N )} F = (F ∩ (T × P )) ∪ {(τ [u] , p [u] ) | [u] ∈ C(N )}∪ {(p, τ [u] ) | [u] ∈ C(N ), p ∈ • [u]} ∪ {(p [t] , t) | t ∈ T } l = l ∪ {(τ [u] , τ ) | [u] ∈ C(N )}.
By Best and Shields, FC(N ) is an FC-net simulating N if N is an EFC-net [START_REF] Best | Some equivalence results for free choice nets and simple nets and on the periodicity of live free choice nets[END_REF].

Let us now determine if EFC-nets remain equivalent to FC-nets when considering concurrency-aware equivalences. As we employ structural conflict nets, two transitions may only fire in a step if they do not share any preplace. Furthermore, the transformation defined above preserves conflict clusters in the sense that C(N ) ⊆ C(FC(N )). Hence, if two transitions belonged to a step of N , they are still part of a step of FC(N ). Formally, the transformation function FC enjoys the property that an EFC-net N and FC(N ) are weak step bisimilar. The weak version of the equivalence is necessary, as FC introduces τ -transitions that do not belong to the original plain EFC-net.

Theorem 1. Let N be a plain EFC-net. Then N ≈ B FC(N ).

The proof of this theorem relies on the observation that the markings of N are also markings of FC(N ). The only difference is that the construction introduces some new places, one per EFC-cluster, that only hold a token if their preceding τ -transition has fired.

R = {(M 1 , M 2 ) | M 1 ∈ [N ∧ M 1 τ -→ * FC(N ) M 2 }

is a weak step bisimulation relation between N and FC(N ).

Thus, EFC-nets remain equivalent to FC-nets under concurrency-aware equivalences, even by using the well-known transformation. Intuitively, this paves the way for FC-net-based analysis for distributed systems being specified by EFCnets. In the following section, we try to repeat this result for behavioral free-choice nets (BFC-nets). Unfortunately, not all BFC-nets exhibit (step) behavior that may be expressed by an equivalent FC-net.

Behavioral Free-Choice

Free-choice may be explored by a behavioral notion. The net in Fig. 2 (c) is neither an FC-net nor an EFC-net. However, in every reachable marking, con-flicting transitions t and u as well as u and v are either enabled or disabled. Although not all conflicting transitions depend on exactly the same resources, the initial conflict situation remains invariant. Once again, this meets the intuition of free-choice. This observation is the basis for behavioral free-choice nets (BFC-nets).

Definition 11 (Behavioral Free-Choice Net). A behavioral free-choice net (BFC-net) is a Petri net N = (P, T, F, M 0 , l) where ∀t, u ∈ T :

• t ∩ • u = ∅ ⇒ ∀M ∈ [N : • t ≤ M ⇔ • u ≤ M .
Every EFC-net is a BFC-net and thus every FC-net is also a BFC-net. However, for BFC-nets, the conflict clustering does not provide the property that C(N ) partitions the set of transitions, e. g., the net depicted in Fig. 2 (c) has two overlapping conflict clusters, namely {t, u} and {u, v}. By merging those overlapping clusters, we reach a partitioning of the set of transitions, called BFC-clusters where u denotes the BFC-cluster of u. Thus, transitions in a BFC-cluster do not necessarily share all of their preplaces, e. g., t and v in Fig. 2 (c) belong to the same BFC-cluster but • t ∩ • v = ∅. However, the BFC-net property ensures that, e. g., in Fig. 2 (c), both t and v are enabled as long as u does not fire. In Fig. 4 (a), another BFC-net is depicted. As before, either all transitions of the BFC-cluster t are enabled or disabled. Thus, without changing the (step) behavior of the BFC-net, we may make each transition t dependent on all places in • t . In order to preserve the markings of the original net, each additional arc is complemented by an arc in the opposite direction. For the net in Fig. 4 (a) we get the EFC-net depicted in Fig. 4 (b). The same implementation idea applied to the BFC-net in Fig. 2 (c) yields the EFC-net depicted in Fig. 3

(b).

For BFC-nets, the result of this construction is always an EFC-net that is interleaving branching time equivalent to the original net [START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF]. Thus, by performing the FC-net construction described in Sect. 3, we get an FC-net that is at least interleaving branching time equivalent to the original BFC-net.

Definition 12 (EFC(N )). Let N = (P, T, F, M 0 , l) be a Petri net. We define EFC(N ) := (P, T, F , M 0 , l) where

F := F ∪ {(p, u), (u, p) | u ∈ T, p ∈ • u , (p, u) ∈ F }.
In Fig. 4, we depicted all intermediate translation steps finally yielding the FCnet depicted in Fig. 4 (c), which is indeed weak step bisimilar to the BFC-net in Fig. 4 (a). Unfortunately, the EFC-net depicted in Fig. 3 (b) is not weak step bisimilar to the net in Fig. 2 (c), as the formerly concurrent transitions t and v are now conflicting. Hence, the proposed construction from the literature does not respect weak step bisimilarity. In general, there is no transformation from the net in Fig. 2 (c) into a step branching time equivalent (E)FC-net. This is due to the pattern, called pure M, the net contains, which has been shown to be stable under step branching time equivalences by van Glabbeek et al. [START_REF] Van Glabbeek | On synchronous and asynchronous interaction in distributed systems[END_REF]. A pure M is characterized by three distinct transitions, t, u, v with

• t ∩ • u = ∅, • u ∩ • v = ∅, and • t ∩ • v = ∅ such
that there is a reachable marking under which all three transitions are enabled. Thus, transitions t and v may fire concurrently while the synchronizing transition u is in conflict with both. In particular, van Glabbeek et al. prove that if a Petri net contains a pure M, then every step failure equivalent [START_REF] Van Glabbeek | Symmetric and asymmetric asynchronous interaction[END_REF] and thus every step ready equivalent [START_REF] Van Glabbeek | On synchronous and asynchronous interaction in distributed systems[END_REF] Petri net contains a pure M. Hence, every step branching time equivalent Petri net containing the net depicted in Fig. 2 (c) is condemned to contain the same pattern again. Fortunately, the containment of pure Ms is no necessary condition for a Petri net to be a BFC-net, e. g., the BFC-net in Fig. 4 (a) does not even have three transitions. Therefore, we devise two subclasses of BFC-nets that do not have pure Ms in the following. First, we restrict BFC-nets to those nets that do not have self-loops. Second, we look at the intersection of BFC-nets and so called asymmetric choice nets in which self-loops are allowed. See again [START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF] for an overview on asymmetric choice nets. Both subclasses turn out to be step branching time equivalent to FC-nets.

BFC-nets without Self-Loops

In this section, we briefly discuss pure Ms in BFC-nets without self-loops. A self-loop is constituted by a transition t and a place p such that t consumes from and produces to p. Definition 13 (Self-Loop). Let N = (P, T, F, M 0 , l) be a Petri net. N has a self-loop iff ∃p ∈ P :

• p ∩ p • = ∅.
If we now consider BFC-nets without any self-loops, we need to reassess our argumentation above on why BFC-nets are not equivalent to FC-nets. Without a self-loop, a pure M is not expressible, because if t or v fired without returning the token to their preplaces they share with u, the overall net would not obey the BFC-net property. Indeed, the construction known from the literature works for BFC-nets without self-loops, proving that BFC-nets without self-loops are step-branching equivalent to (E)FC-nets.

Theorem 2. Let N be a plain BFC-net without self-loops. Then EFC(N ) ≈ B N .

In order to prove that the construction does not change the step behavior of N , it is sufficient to show that t u implies t = u for all t, u ∈ T . Suppose, there are transitions contradicting this requirement. If there is a reachable marking enabling t and u, then after firing t, u is enabled while t is not, contradicting that N is a BFC-net. Therefore, the EFC-net construction does not restrict the set of enabled steps from reachable markings. The remaining proof follows the same principles as the proof of Theorem 3, provided in the appendix. Next, we discuss a subclass that allows self-loops in BFC-nets but restricts the class structurally to not contain Ms.

BFC-nets and Asymmetric Choice

The condition for a Petri net to be an EFC-net may be reformulated in terms of places, yielding exactly the same net class as by Def. 9 [START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF]. In this definition, a Petri net is an EFC-net iff for all places p and q it holds that p • ∩ q • = ∅ implies that p • = q • . In an asymmetric choice net (AC-net), this restriction is weakened to an alternative between the two set-inclusions between p • and q • . Before discussing the combination of BFC-nets and AC-nets, we clarify the relation between AC-nets and FC-nets.

Definition 14 (Asymmetric Choice Net). A Petri net N = (P, T, F, M 0 , l) is an asymmetric choice net (AC-net) iff ∀p, q ∈ P :

p • ∩ q • = ∅ ⇒ p • ⊆ q • ∨ q • ⊆ p • .
In case p • ⊆ q • but q • ⊆ p • , all transitions in q • are enabled if at least p and q hold tokens. This restriction hardly enforces the concepts of free-choice, as it does not require conflicting transitions to be chosen freely. However, the Petri net depicted in Fig. 2 (a) shows an example AC-net, which may be simulated by an FC-net. We discuss this transformation in Sect. 5. Considering the same net in a larger context, it is unclear whether a token eventually occurs on the second input place of u. The AC-net in Fig. 5 (a) shows an example context. The choice between transitions t and u does only occur if transition x fires in advance. In an adversary scenario, transition x might only fire if transition t has fired, which makes u unable to fire at all. In the literature, such a situation is called (asymmetric) confusion [START_REF] Rozenberg | Petri nets: Basic notions, structure, behaviour[END_REF], which may not be simulated by any FCnet, as choices may never occur conditionally. In general, we characterize such conditional choices by the notion of partially and fully reachable Ns. Here, the existence of a subnet like the one in Fig. 2 (a) is expected and two distinct markings, one under which t is enabled and one enabling t and u.

Definition 15 (Partially and Fully Reachable N). Let N = (P, T, F, M 0 , l) be a Petri net. (t, u) ∈ T 2 is a partially and fully reachable

N iff • t ∩ • u = ∅, | • u| > 1, and ∃M t , M ∈ [N : • t ≤ M t ∧ • u ≤ M t ∧ • {t, u} ≤ M .
Note that this notion does not only characterize asymmetric confusion patterns, but also nets as the one depicted in Fig. 5 (b). Just as in the case of pure Ms, partially and fully reachable Ns are stable w. r. t. step branching time equivalences.

Proposition 1. Let N be a plain Petri net with a partially and fully reachable N. Then for all plain-labeled Petri nets N with N ≈ F N it holds that N has a partially and fully reachable N.

Proof. Let N = (P, T, F, M 0 , l) and (t, u) a partially and fully reachable N of N , i. e., there exist reachable markings M t and M such that M t enables t, but not and M enables both. Thus, there is a σ such that M 0 σ =⇒ M t and since N is plain, and hence deterministic [START_REF] Vidal-Naquet | Deterministic languages of petri nets[END_REF], (1) (σ, X) ∈ F(N ) implies that {l(t)} ∈ X and there exists (σ, X) with {l(u)} ∈ X. From the existence of M we deduce that (2) there is a σ such that M 0 σ =⇒ M and (3) (σ , X) ∈ F(N ) implies that {l(t)} ∈ X ∧ {l(u)} ∈ X. As N is a structural conflict net, (4) there exists (σ , X) ∈ F(N ) such that {l(t), l(u)} ∈ X.

Let N = (P , T , F , M 0 , l ) be a Petri net with N ≈ F N , i. e., F(N ) = F(N ). Therefore, F(N ) obeys ( 1)-( 4). Hence, there exist transitions t , u ∈ T with l (t ) = l(t) and l (u ) = l(u). By ( 3) and ( 4), we have that • t ∩ • u = ∅. By (1), we get that there is a place p ∈

• u \ • t thus | • u | > 1.
By [START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF], there is a marking M t with M 0 σ =⇒ M t and • t ≤ M t ∧ • u ≤ M t , as otherwise there would be a failure pair (σ, X) ∈ F(N ) with {l (t )} ∈ X. By (2), there is a marking M with M 0 σ =⇒ M and by (3) • t ≤ M ∧ • u ≤ M . By (4) {t , u } is no step from M . Summarizing, N has a partially and fully reachable N.

Corollary 1. There is no transformation function from plain AC-nets to plainlabeled step branching time equivalent FC-nets.

However, the BFC-net in Fig. 2 (c) does not respect the restrictions as imposed on AC-nets. In general, such structures may not occur in an AC-net and conversely, partially and fully reachable Ns are ruled out in BFC-nets, which paves the way for the following theorem. Theorem 3. Let N be a plain BFC-net and an AC-net. Then EFC(N ) ≈ B N .

Note that Best and Shields already prove that EFC yields an EFC-net for BFCnets [START_REF] Best | Some equivalence results for free choice nets and simple nets and on the periodicity of live free choice nets[END_REF]. Concerning the proof of Theorem 3, we benefit from the construction given in Def. 12, adding no more places to the original net. Thus, every marking of N is also a marking of EFC(N ). Furthermore, the construction does not change the enabledness condition for transitions, and it does not even increase or decrease formerly existing steps. Thus, the desired weak step bisimulation between N and EFC(N

) is R = {(M, M ) | M ∈ [N }.
The proof that R is a weak step bisimulation is provided in the appendix.

Throughout the last section, we have seen two subclasses of BFC-nets that are step branching time equivalent to FC-nets. However, BFC-nets do not represent a reasonable basis for the step branching time closure of FC-nets, i. e., there are non-BFC-nets being behaviorally equivalent to FC-nets, e. g., the net depicted in Fig. 2 (a). In this section, we analyze a Petri net class that appears in the context of investigations on synchronous and asynchronous interaction. R. van Glabbeek et al. introduced this class that does not distinguish simultaneous and delayed token removals from more than one place on a behavioral level [START_REF] Van Glabbeek | On synchronous and asynchronous interaction in distributed systems[END_REF]. Each place of a Petri net is assumed to reside on an individual location. If a transition has only one preplace, it may be assigned to the same location. Two transitions reside on a shared location if they share a preplace that is allowed on the same location. Thus, whenever a transition synchronizes more than one place, i. e., more than one location, it resides on a different location than any of its preplaces. Interaction delays between locations are simulated by an additional τ -transition and place on each arc crossing location borders, an asynchronous implementation. A Petri net is symmetrically asynchronous iff it is step failure equivalent to its asynchronous implementation.

Definition 16 (Symmetric Asynchrony [START_REF] Van Glabbeek | On synchronous and asynchronous interaction in distributed systems[END_REF]). Let L be a set of locations and N = (P, T, F, M 0 , l) be a Petri net. A (distribution) function λ : (P ∪ T ) → L is a symmetric distribution on N when λ(p) = λ(q) for p, q ∈ P only if p = q, λ(t) = λ(p) for t ∈ T, p ∈ P only if • t = {p} and λ(t) = λ(u) for t, u ∈ T only if t = u or ∃p ∈ P : λ(t) = λ(p) = λ(u), I λ (N ) := (P ∪ P τ , T ∪ T τ , F , M 0 , l) is the asynchronous implementation (w. r. t. λ) of N iff

P τ := {s t | t ∈ T, s ∈ • t, λ(s) = λ(t)}, T τ := {t s | t ∈ T, s ∈ • t, λ(s) = λ(t)}, F := {(t, s) | t ∈ T, s ∈ t • } ∪ {(s, t) | s ∈ • t, λ(s) = λ(t)}∪ {(s, t s ), (t s , s t ), (s t , t) | t ∈ T, s ∈ • t, λ(s) = λ(t)}, l (t)
:= l(t) if t ∈ T τ otherwise. N is symmetrically asynchronous iff there exists a symmetric distribution λ on N such that N ≈ F I λ (N ). R. van Glabbeek et al. prove that a Petri net is symmetrically asynchronous iff there is a symmetric distribution λ and the Petri net has no distributed conflict w. r. t. λ [START_REF] Van Glabbeek | On synchronous and asynchronous interaction in distributed systems[END_REF]. A Petri net is said to have a distributed conflict w. r. t. λ iff there are two distinct transitions t, u with • t∩ • u = ∅, λ(t) = λ(u), and there is a reachable marking enabling t. Another characterization of symmetrically asynchronous Petri nets is given in terms of a Petri net pattern, called partially reachable N [START_REF] Van Glabbeek | On synchronous and asynchronous interaction in distributed systems[END_REF], which follows the definition given in Def. 15, leaving out the existence of the marking M (full reachability). All the nets depicted in Fig. 2 have partially reachable Ns, obstructing symmetric asynchrony. R. van Glabbeek et al. conjecture that there is a strong relation between symmetrically asynchronous nets and FC-nets [START_REF] Van Glabbeek | Symmetric and asymmetric asynchronous interaction[END_REF], which we finally prove in the following. Given a symmetrically asynchronous Petri net N = (P, T, F, M 0 , l), i. e., there is a symmetrical distribution λ : P ∪T → L such that N has no distributed conflict w. r. t. λ. We transform N under λ by FC sym (N ) = (P, T , F , M 0 , l) where

-T := {t ∈ T | ∀p ∈ • t : ∀u ∈ p • : λ(p) = λ(u) ∨ u = t} and -F := F ∩ ((P × T ) ∪ ( T × P )).
This transformation yields an FC-net by removing transitions obstructing the FC-net properties.

Lemma 1. Let N be a symmetrically asynchronous Petri net. Then, FC sym (N ) is an FC-net.

Proof. Let N = (P, T, F, M 0 , l) be a symmetrically asynchronous Petri net and λ the required symmetrical distribution. N has no distributed conflict w. r. t.

λ [7], i. e., ∀t, u ∈ T ∀p ∈ • t ∩ • u : t = u ∨ λ(p) = λ(u)∨ ∃M ∈ [N : • t ≤ M .
Let N = FC sym (N ) with set of transitions T and arc relation F . We show that for all p ∈ P and all t ∈ T , (p, t) ∈ F implies • t = {p} or p • = {t}. Assume there is a place p and a transition t with (p, t) ∈ F , but • t = {p} and p • = {t}. Hence, there exists a place q = p with q ∈ • t and a transition u ∈ T with t = u and u ∈ p • . As λ is symmetrical, p is not co-located with q and t, q is not colocated with u and t, and hence, t is not co-located with u. There are two cases to consider, (1) λ(p) = λ(u) and ( 2) λ(p) = λ(u). If (1), then u ∈ T , because by definition of T , for all transitions in p • , it must hold that they are co-located with p or they are equal to u. But u = t, t ∈ p • and λ(p) = λ(t). If (2), then u, t ∈ T by definition of T . In detail, t ∈ T , as there is a transition u ∈ p • with λ(p) = λ(u) (by assumption (2)). u ∈ T , as there is a transition, t ∈ p • , with λ(t) = λ(p) (by λ being symmetrical). Hence, either {t} = p • or t does not even exist. Thus, FC sym (N ) is an FC-net.

Fortunately, none of the removed transitions takes part in actual behavior, as all of them are dead transitions, i. e., there is no reachable marking enabling them. Lemma 2. Let N = (P, T, F, M 0 , l) be a symmetrically asynchronous Petri net and FC sym (N ) = (P, T , F , M 0 , l). Then for all t ∈ T \ T there is no M ∈ [N such that M [{t} .

Proof. Assume there is a t ∈ T \ T and a marking M ∈ [N such that t is enabled under M . By definition of T , there is a p ∈ • t and a u ∈ p • such that λ(p) = λ(u) and u = t. But M enabled t, contradicting the assumption that N is symmetrically asynchronous, i. e., N has no distributed conflict. Hence, FC sym yields step branching time equivalent FC-nets. This theorem directly follows from Lemma 2. As every FC-net is also symmetrically asynchronous, we get the following correspondence between the step branching time closure of FC-nets and of symmetrically asynchronous nets.

Corollary 2. Let N be a plain Petri net. N is weak step bisimilar to a plainlabeled FC-net iff N is weak step bisimilar to a plain-labeled symmetrically asynchronous Petri net.

Conclusions and Future Work

We provided an overview on well-known free-choice related Petri net classes and their transformations between them. Our goal was to analyze their relations under concurrency-aware equivalences, namely step branching time equivalences. EFC-nets are equivalent to FC-nets while BFC-nets contain critical structures not expressible by any FC-net. We proved that two subclasses of BFC-nets, namely self-loop free BFC-nets and BFC-nets that are also AC-nets, are behaviorally equivalent to FC-nets respecting concurrent steps. Finally, we proved that the closure of step branching time equivalent FC-nets relies on the closure of symmetrically asynchronous Petri nets, a syntactically larger class than FC-nets.

FC-nets come with efficient analysis algorithms that are also useful for the analysis of distributed systems. Positive results in this paper may be used to transport many of the analysis techniques of FC-nets to broader net classes like EFC-nets or BFC-nets. Negative results we pointed to or actually proved, sketch a limit of efficient analyzability, as Best stated that many of the free-choice related results do not hold for net classes beyond free-choice [START_REF] Best | Structure theory of petri nets: the free choice hiatus[END_REF].

For future work, we plan to tackle the closure of symmetrically asynchronous Petri nets, i. e., FC-nets (cf. Corollary 2). In [START_REF] Mennicke | Strong Distributability Criteria for Petri Nets[END_REF], partial closure and remaining problematic structures are provided by equating symmetrically asynchronous Petri nets with distributed systems and asking for the class of distributable Petri nets. For another notion of distributed Petri nets related to the aforementioned pure M, such a closure is provided by van Glabbeek et al. in terms of ST bisimulation, a strong equivalence taking causality into account [START_REF] Van Glabbeek | On characterising distributability[END_REF]. The EFC-net construction presented in this paper adds causality. Thus, a causality-preserving transformation remains to be found if possible.

N

  denotes the reflexive and transitive closure of τ -→ N .

Fig. 2 :

 2 Fig.2: Three nets that are not FC-nets.

Fig. 4 :

 4 Fig.4: From BFC-nets to FC-nets.

Fig. 5 :

 5 Fig. 5: Two AC-nets having a Partially and Fully Reachable N.

Theorem 4 .

 4 Let N be a plain symmetrically asynchronous Petri net. Then N ≈ B FC sym (N ).

This work is supported by the DFG (German Research Foundation).

. . .

A Proof of Theorem 1

Let N = (P, T, F, M 0 , l) be a plain EFC-net and N = FC(N ) = (P , T , F , M 0 , l ). We prove that R

is a bisimulation. Note that P ⊆ P and T ⊆ T . (M 0 , M 0 ) ∈ R, as M 0 = M 0 . Let (M 1 , M 2 ) ∈ R. As N is τ -free, there are three cases to consider:

as all outgoing arcs of transitions are preserved. By definition, (M Hence, R is a weak step bisimulation between N and FC(N ).

B Proof of Theorem 3

Let N = (P, T, F, M 0 , l) be a BFC-AC-net specification and EFC(N ) = N = (P, T, F , M 0 , l). We prove that R = {(M, M ) | M ∈ [N } is a weak step bisimulation between N and N . By definition, (M 0 , M 0 ) ∈ R. Let (M 1 , M 2 ) ∈ R. The cases for τ -steps are obsolete, as N and N are plain.

as M 2 = M 1 and tokens that are consumed due to the construction of N are reproduced. Additionally, the original outgoing arcs of transitions are preserved. As N is a structural conflict net and due to the construction, for transitions t 1 , t 2 ∈ G it holds that • t 1 ∩ • t 2 = ∅. It remains to be shown that Ĝ = G is enabled by M 2 , i. e., • Ĝ ≤ M 2 . Let t ∈ Ĝ with t = t. The t/ Ĝ notation just helps distinguishing between elements of N and N . As in N , no arcs were removed, it holds that | • t| ≥ | • t|. In case of equality, the claim holds and G may fire under M 2 . If | • t| > | • t|, then there are places p, q ∈ P and a transition u ∈ T such that p ∈ • t ∩ • u, q ∈ • t but q ∈ • u -due to the fact that N is an AC-net. Hence, in N there is an additional arc from q to t. As N is a BFC-net, t is enabled iff u is enabled and hence, q ∈ M 1 . Thus, q ∈ M 2 . In conclusion • t ≤ M 2 thus • Ĝ ≤ M 2 , i. e., Ĝ is enabled by M 2 and may fire, producing a new marking M 2 with the properties described above.

M 2

A

-→ N M 2 , i. e., there is a step G from M 2 to M 2 and l(G) = A. N is τ -free and therefore, we need to give a marking

As before, a t in N has less or equal incoming arcs than t in N . As, M 2 = M 1 by definition of R, G is a step from M 1 to a marking M 1 . Every token that is consumed by some t in N , due to the construction of N , is reproduced in N . In N such tokens are not even consumed by t. The original postsets of transitions are preserved and hence, M 1 [G N M 1 and M 2 = M 1 thus (M 1 , M 2 ) ∈ R.