Wyniki wyszukiwania - BazTech

1

From Box Algebra to Interval Temporal Logic

Klaudel Hanna, Koutny Maciej, Duan Zhenhua, Moszkowski Ben

Fundamenta Informaticae

|

2019

|

Vol. 167, nr 4

323--354

EN

In this paper, we further develop a recently introduced semantic link between temporal logics and Petri nets. We focus on two specific formalisms, Interval Temporal Logic (ITL) and Box Algebra (BA), which are closely related by their compositional approach to constructing system descriptions. The overall goal of our investigation is to translate Petri nets into behaviourally equivalent logical formulas. As a result, the analysis of system properties can be carried out using either of the two formalisms, exploiting their respective strengths and powerful tool support. The contribution of this paper is twofold. First, we extend the existing translation from BA to ITL, by removing restrictions concerning the way control flow of concurrent system is modelled, and by allowing a fully general synchronisation operator. Second, we strengthen the notion of equivalence between a Petri net and the corresponding logical formula by proving such an equivalence at the level of transition-based executions of Petri nets rather than just by looking at their labels. We also show that the complexity of the proposed translation compares favourably with the complexity of the translation from BA expressions to Petri nets.

2

Characterising Concurrent Histories

Janicki R., Kleijn J., Koutny M., Mikulski Ł.

Fundamenta Informaticae

|

2015

|

Vol. 139, nr 1

21--42

EN

Non-interleaving semantics of concurrent systems is often expressed using posets, where causally related events are ordered and concurrent events are unordered. Each causal poset describes a unique concurrent history, i.e., a set of executions, expressed as sequences or step sequences, that are consistent with it. Moreover, a poset captures all precedence-based invariant relationships between the events in the executions belonging to its concurrent history. However, concurrent histories in general may be too intricate to be described solely in terms of causal posets. In this paper, we introduce and investigate generalised mutex order structures which can capture the invariant causal relationships in any concurrent history consisting of step sequence executions. Each such structure comprises two relations, viz. interleaving/mutex and weak causality. As our main result we prove that each generalised mutex order structure is the intersection of the step sequence executions which are consistent with it.

3

Mutex Causality in Processes and Traces of General Elementary Nets

Kleijn J., Koutny M.

Fundamenta Informaticae

|

2013

|

Vol. 122, nr 1-2

119--146

EN

A concurrent history represented by a causality structure that captures the intrinsic, invariant dependencies between its actions, can be interpreted as defining a set of closely related observations (e.g., step sequences). Depending on the relationships observed in the histories of a system, the concurrency paradigm to which it adheres may be identified, with different concurrency paradigms underpinned by different kinds of causality structures. Elementary net systems with inhibitor arcs and mutex arcs (ENIM-systems) are a system model that through its process semantics and associated causality structures fits the least restrictive concurrency paradigm. One can also investigate the abstract behaviour of an ENIM-system by grouping together step sequences in equivalence classes (generalised comtraces) using the structural relations between its transitions. The resulting concurrent histories of the ENIM-system are consistent with the generalised stratified order structures underlying its processes. The paper establishes a link between ENIM-systems and trace theory allowing one to discuss different observations of concurrent behaviour in a way that is consistent with the causality semantics defined by the operationally defined processes.