Title :
Property preserving transition refinement with concurrent runs: an example
Author_Institution :
Inst. fur Informatik, Humboldt-Univ., Berlin, Germany
Abstract :
We suggest a new notion of behavior preserving transition refinement based on partial order semantics. Furthermore, we discuss how to prove the correctness of a transition refinement step. Our results are formalized in the setting of Petri nets. We use Petri nets because they have a canonical partial order semantics, which is defined by concurrent runs
Keywords :
Petri nets; concurrency theory; distributed algorithms; distributed processing; temporal logic; Petri nets; distributed systems; partial order semantics; safe systems; transition refinement; Asynchronous communication; Concurrent computing; Crosstalk; Petri nets; Protocols;
Conference_Titel :
Application of Concurrency to System Design, 2001. Proceedings. 2001 International Conference on
Conference_Location :
Newcastle upon Tyne
Print_ISBN :
0-7695-1071-X
DOI :
10.1109/CSD.2001.981766
