Proving Nets Correct via Cause-Effect Structures (An Experiment)

Issue title: Concurrency Specification and Programming (CS&P'2002), Part 1

Article type: Research Article

Authors: Czaja, Ludwik

Affiliations: Institute of Informatics, Warsaw University, Warsaw, Poland

Abstract: Proving safety and liveness of parallel systems is of unquestionable importance in system construction activity. A proof method for systems represented by nets (cause-effect structures and Petri nets) is proposed. Its outline is the following. (1) Let a problem specification as a formal theory i.e. a language system with specific relation symbols (operations, in particular), axioms and first-order inference rules be given. For each symbol introduce a class of atomic c-e structures (counterpart of Petri net transitions) to be the symbol's operational representative. (2) Using algebraic calculus of cause-effect structures, construct - from the atoms - a c-e structure and equivalent net intended to behave in accordance with the axioms (a mechanical step); (3) From the cause-effect structure just constructed, infer an algebraic structure and prove it to be a model (in terms of model theory) of the axiomatic system specifying the problem.

Keywords: Cause-effect structures, Petri nets, specification, correctness, model theory

Journal: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 165-183, 2003