Deriving a Graph Rewriting System from a Complete Finite Prefix of an Unfolding

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Downloads (Pure)

Abstract

The starting point of this paper is McMillan's complete finite prefix of an unfolding that has been obtained from a Petri net or a process algebra expression. The paper addresses the question of how to obtain the (possibly infinite) system behaviour from the complete finite prefix. An algorithm is presented to derive from the prefix a graph rewriting system that can be used to construct the unfolding. It is shown how to generate event sequences from the graph rewriting system which is important for constructing an interactive simulator. Finally it is indicated how the graph rewriting system yields a transition system that can be used for model checking and test derivation.
Original languageEnglish
Title of host publicationEXPRESS'99
Subtitle of host publication6th International Workshop on Expressiveness in Concurrency
EditorsIlaria Castellani, Björn Victor
PublisherElsevier
Pages24-41
Number of pages17
DOIs
Publication statusPublished - 1999
Event6th International Workshop on Expressiveness in Concurrency, EXPRESS 1999 - Eindhoven, Netherlands
Duration: 23 Aug 199923 Aug 1999
Conference number: 6

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
Volume27
ISSN (Print)1571-0661

Workshop

Workshop6th International Workshop on Expressiveness in Concurrency, EXPRESS 1999
Abbreviated titleEXPRESS
CountryNetherlands
CityEindhoven
Period23/08/9923/08/99

Fingerprint

Model checking
Petri nets
Algebra
Simulators

Keywords

  • FMT-MC: MODEL CHECKING
  • FMT-PA: PROCESS ALGEBRAS

Cite this

Langerak, R. (1999). Deriving a Graph Rewriting System from a Complete Finite Prefix of an Unfolding. In I. Castellani, & B. Victor (Eds.), EXPRESS'99: 6th International Workshop on Expressiveness in Concurrency (pp. 24-41). (Electronic Notes in Theoretical Computer Science; Vol. 27). Elsevier. https://doi.org/10.1016/S1571-0661(05)80293-2
Langerak, Rom. / Deriving a Graph Rewriting System from a Complete Finite Prefix of an Unfolding. EXPRESS'99: 6th International Workshop on Expressiveness in Concurrency. editor / Ilaria Castellani ; Björn Victor. Elsevier, 1999. pp. 24-41 (Electronic Notes in Theoretical Computer Science).
@inproceedings{676b737a0e604573a4743829af865985,
title = "Deriving a Graph Rewriting System from a Complete Finite Prefix of an Unfolding",
abstract = "The starting point of this paper is McMillan's complete finite prefix of an unfolding that has been obtained from a Petri net or a process algebra expression. The paper addresses the question of how to obtain the (possibly infinite) system behaviour from the complete finite prefix. An algorithm is presented to derive from the prefix a graph rewriting system that can be used to construct the unfolding. It is shown how to generate event sequences from the graph rewriting system which is important for constructing an interactive simulator. Finally it is indicated how the graph rewriting system yields a transition system that can be used for model checking and test derivation.",
keywords = "FMT-MC: MODEL CHECKING, FMT-PA: PROCESS ALGEBRAS",
author = "Rom Langerak",
year = "1999",
doi = "10.1016/S1571-0661(05)80293-2",
language = "English",
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Elsevier",
pages = "24--41",
editor = "Ilaria Castellani and Bj{\"o}rn Victor",
booktitle = "EXPRESS'99",

}

Langerak, R 1999, Deriving a Graph Rewriting System from a Complete Finite Prefix of an Unfolding. in I Castellani & B Victor (eds), EXPRESS'99: 6th International Workshop on Expressiveness in Concurrency. Electronic Notes in Theoretical Computer Science, vol. 27, Elsevier, pp. 24-41, 6th International Workshop on Expressiveness in Concurrency, EXPRESS 1999, Eindhoven, Netherlands, 23/08/99. https://doi.org/10.1016/S1571-0661(05)80293-2

Deriving a Graph Rewriting System from a Complete Finite Prefix of an Unfolding. / Langerak, Rom.

EXPRESS'99: 6th International Workshop on Expressiveness in Concurrency. ed. / Ilaria Castellani; Björn Victor. Elsevier, 1999. p. 24-41 (Electronic Notes in Theoretical Computer Science; Vol. 27).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Deriving a Graph Rewriting System from a Complete Finite Prefix of an Unfolding

AU - Langerak, Rom

PY - 1999

Y1 - 1999

N2 - The starting point of this paper is McMillan's complete finite prefix of an unfolding that has been obtained from a Petri net or a process algebra expression. The paper addresses the question of how to obtain the (possibly infinite) system behaviour from the complete finite prefix. An algorithm is presented to derive from the prefix a graph rewriting system that can be used to construct the unfolding. It is shown how to generate event sequences from the graph rewriting system which is important for constructing an interactive simulator. Finally it is indicated how the graph rewriting system yields a transition system that can be used for model checking and test derivation.

AB - The starting point of this paper is McMillan's complete finite prefix of an unfolding that has been obtained from a Petri net or a process algebra expression. The paper addresses the question of how to obtain the (possibly infinite) system behaviour from the complete finite prefix. An algorithm is presented to derive from the prefix a graph rewriting system that can be used to construct the unfolding. It is shown how to generate event sequences from the graph rewriting system which is important for constructing an interactive simulator. Finally it is indicated how the graph rewriting system yields a transition system that can be used for model checking and test derivation.

KW - FMT-MC: MODEL CHECKING

KW - FMT-PA: PROCESS ALGEBRAS

U2 - 10.1016/S1571-0661(05)80293-2

DO - 10.1016/S1571-0661(05)80293-2

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 24

EP - 41

BT - EXPRESS'99

A2 - Castellani, Ilaria

A2 - Victor, Björn

PB - Elsevier

ER -

Langerak R. Deriving a Graph Rewriting System from a Complete Finite Prefix of an Unfolding. In Castellani I, Victor B, editors, EXPRESS'99: 6th International Workshop on Expressiveness in Concurrency. Elsevier. 1999. p. 24-41. (Electronic Notes in Theoretical Computer Science). https://doi.org/10.1016/S1571-0661(05)80293-2