Top

Programming and Computer Software

Published in:

01-07-2020

Testing Equivalences of Time Petri Nets

Authors: E. N. Bozhenkova, I. B. Virbitskaite

Published in: Programming and Computer Software | Issue 4/2020

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

In the paper, we study a family of testing equivalences in interleaving, partial-order semantics, and combined semantics in the context of safe time Petri nets (elementary net systems whose transitions are labeled with time firing intervals, can fire only if their lower time bounds are attained, and are forced to fire when their upper time bounds are reached). For this purpose, the following three representations of behavior of safe time Petri nets are developed: sequences of firings of net transitions, which represent interleaving semantics; time causal processes, from which partial orders are derived; and time causal tree, whose nodes are sequences of transition firings and arcs are labeled by information about partial orders. We establish relationships between these equivalences and show that semantics of time causal processes and time causal trees coincide.

next article Dedicative Verification of Reflex Programs

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

For convenience of subsequent definitions, we do not use the classical definition: a transition \(t \in T\) is enabled at a marking M if \(^{ \bullet }t \subseteq M\) and \(M \cap {{t}^{ \bullet }} = \emptyset \). The second requirement will be introduced in the definition of the contact-free property.

Note that, if the base Petri net N is contact-free, then the time Petri net \(\mathcal{T}\mathcal{N}\) is also contact-free, but the converse is not true.

The time-progressive property guarantees correctness of the modified definition of the contact-free property.

A (labeled overAct) time partially ordered set (poset) is a tuple \(\eta = (X, \preccurlyeq ,\lambda ,\tau )\) consisting of a finite set of elements X; reflexive, asymmetric, and transitive relation \( \preccurlyeq \); a labeling function λ: \(X\, \to \,Act\); and a time function \(\tau {\kern 1pt} :\;X \to T\) such that \(e\, \preccurlyeq \,e'\, \Rightarrow \,\tau (e)\, \leqslant \,\tau (e')\). Let \(\tau (\eta ) = \max\{ \tau (x)\,|\,x \in X\} \).

Two time posets \(\eta = (X, \preccurlyeq ,\lambda ,\tau )\) and \(\eta ' = (X', \preccurlyeq {\kern 1pt} ',\lambda ',\tau ')\) are isomorphic (denoted as \(\eta \simeq \eta '\)) if there exists a bijection \(\beta {\kern 1pt} :\;X \to X'\) such that (a) \(x \preccurlyeq y \Leftrightarrow \beta (x) \preccurlyeq {\kern 1pt} '\,\beta (y)\) for all \(x,y \in X\) and (b) \(\lambda (x) = \lambda '(\beta (x))\) and \(\tau (x) = \tau '(\beta (x))\) for all \(x \in X\).

We define \(path(\epsilon ) = \epsilon \). Note that, in a \(TCT(\mathcal{T}\mathcal{N})\), for any node \(\sigma \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})\), there exists a path from the root to a node \(\sigma \).

A time poset \(\eta = (X, \preccurlyeq ,\lambda ,\tau )\) is called prefix of a time poset \(\eta ' = (X', \preccurlyeq ',\lambda ',\tau ')\) (denoted as \(\eta \prec \cdot \eta '\)) if \(X \subseteq X'\), \(X{{'\backslash }}X = \{ x\} \), \( \preccurlyeq = \preccurlyeq ' \cap (X \times X)\), \(\lambda = \lambda '{{{\text{|}}}_{X}}\), \(\tau = \tau '{{{\text{|}}}_{X}}\), and x is the greatest with respect to \( \preccurlyeq '\) element of \(X'\)

De Nicola, R. and Hennessy, M., Testing equivalence for processes, Theoret. Comput. Sci., 1984, vol. 34, pp. 83–133.MathSciNetCrossRef

De Nicola, R., Extensional equivalences for transition systems, Acta Inform., 1987, vol. 24, no. 2, pp. 211–237.MathSciNetCrossRef

Cleaveland, R. and Hennessy, M., Testing equivalence as a bisimulation equivalence, Lect. Notes Comp. Sci., 1989, vol. 407, pp. 11–23.CrossRef

Pomello, L., Rozenberg, G., and Simone, C., A survey of equivalence notions for net based systems, Lect. Notes Comp. Sci., 1992, vol. 609, pp. 410–472.MathSciNetCrossRef

Aceto, L., De Nicola, R., and Fantechi, A., Testing equivalences for event structures, Lect. Notes Comp. Sci., 1987, vol. 280, pp. 1–20.MathSciNetCrossRef

Goltz, U. and Wehrheim, H., Causal testing, Lect. Notes Comp. Sci., 1996, vol. 1113, pp. 394–406.MathSciNetCrossRef

Aceto, L., History preserving, causal and mixed-ordering equivalence over stable event structures, Fund. Inform., 1992, vol. 17, no. 4, pp. 319–331.MathSciNetMATH

Darondeau, Ph. and Degano, P., Refinement of actions in event structures and causal trees, Theoret. Comput. Sci., 1993, vol. 118, no. 1, pp. 21–48.MathSciNetCrossRef

Nielsen, M., Rozenberg, G., and Thiagarajan, P.S., Behavioural notions for elementary net systems, Distrib. Comput., 1990, vol. 4, no. 1, pp. 45–57.MathSciNetCrossRef

10.

Hoogers, P.W., Kleijn, H.C.M., and Thiagarajan, P.S., An event structure semantics for general Petri nets, Theoret. Comput. Sci., 1996, vol. 153, nos 1–2, pp. 129–170.

11.

van Glabbeek, R.J., Goltz, U., and Schicke, J.-W., On causal semantics of Petri nets, Lect. Notes Comp. Sci., 2011, vol. 6901, pp. 43–59.MathSciNetCrossRef

12.

Cleaveland, R. and Zwarico, A.E., A theory of testing for real-time, Proc. of 6th IEEE Symp. on Logic in Comput. Sci. (LICS'91), Amsterdam, The Netherlands, 1991.

13.

Llana, L. and de Frutos, D., Denotational semantics for timed testing, Lect. Notes Comp. Sci., 1997, vol. 1233, pp. 368–382.CrossRef

14.

Hennessy, M. and Regan, T., A process algebra for timed systems, Inform. and Comput., 1995, vol. 117, pp. 221–239.MathSciNetCrossRef

15.

Corradini, F., Vogler, W., and Jenner, L., Comparing the worst-case efficiency of asynchronous systems with PAFAS, Acta Inform., 2002, vol. 38, pp. 735–792.MathSciNetCrossRef

16.

Bihler, E. and Vogler, W., Timed Petri nets: Efficiency of asynchronous systems, Lect. Notes Comp. Sci., 2004, vol. 3185, pp. 25–58.CrossRef

17.

Murphy, D., Time and duration in noninterleaving concurrency, Fund. Inform., 1993, vol. 19, pp. 403–416.MathSciNetMATH

18.

Andreeva, M., Bozhenkova, E., and Virbitskaite, I., Analysis of timed concurrent models based on testing equivalence, Fund. Inform., 2000, vol. 43, pp. 1–20.MathSciNetCrossRef

19.

Andreeva, M. and Virbitskaite, I., Timed equivalences for timed event structures, Lect. Notes Comp. Sci., 2005, vol. 3606, pp. 16–25.CrossRef

20.

Andreeva, M. and Virbitskaite, I., Observational equivalences for timed stable event structures, Fund. Inform., 2006, vol. 72, pp. 1–19.MathSciNetMATH

21.

Valero, V., de Frutos, D., and Cuartero, F., Timed processes of timed Petri nets, Lect. Notes Comp. Sci., 1995, vol. 935, pp. 490–509.MathSciNetCrossRef

22.

Virbitskaite, I.B., Borovlev, V.A., and Popova-Zeugmann, L., “Truly concurrent” and nondeterministic semantics of discrete-time Petri nets, Program. Comput. Software, 2016, no. 4, pp. 187–197.

23.

Aura, T. and Lilius, J., A causal semantics for time petri nets, Theoret. Comput. Sci., 2000, vol. 243, nos 1–2, pp. 409–447.

24.

Bushin, D.I. and Virbitskaite, I.B., Comparative trace semantics of time Petri nets, Program. Comput. Software, 2015, no. 3, pp. 131–139.

25.

Virbitskaite, I., Bushin, D., and Best, E., True concurrent equivalences in time Petri nets, Fund. Inform., 2016, vol. 149, no. 4, pp. 401–418.MathSciNetCrossRef

Title: Testing Equivalences of Time Petri Nets
Authors: E. N. Bozhenkova
I. B. Virbitskaite
Publication date: 01-07-2020
Publisher: Pleiades Publishing
Published in: Programming and Computer Software / Issue 4/2020
Print ISSN: 0361-7688
Electronic ISSN: 1608-3261
DOI: https://doi.org/10.1134/S0361768820040040

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Technik"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 4/2020

Dynamic Program Analysis Tools in GCC and CLANG Compilers

Survey of Nvidia RTX Technology

Dedicative Verification of Reflex Programs

Using a System of Heterogeneous Ontology Design Patterns to Develop Ontologies of Scientific Subject Domains

Premium Partner