Proof systems for infinite behaviours (Q1193598)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Proof systems for infinite behaviours |
scientific article |
Statements
Proof systems for infinite behaviours (English)
0 references
27 September 1992
0 references
The paper suggests several generalizations of testing to \(\omega\)- behaviours of communicating processes, analyses the logical complexity of the testing equivalences, and establishes on that basis a connection with proof systems. Section 2 supplies infinitary tests with infinitary results for the equality of linear \(\omega\)-behaviours in pure CCS. Section 3 contains an introduction to \(\omega\)-logic and recalls the strong connection between \(\Pi^ 1_ 1\) and the \(\omega\)-rule. Section 4 establishes a mutual reduction between \(\Pi^ 1_ 2\) formulas of arithmetic and formulas \(p\approx q\), where \(\approx\) is the equivalence over CCS programs induced by tests defined in section 2; it is concluded therefrom that complete systems of \(\omega\)-proofs for \(\approx\) cannot exist. Sections 5 and 6 investigate the logical complexity of two alternative equivalences based on families of finitary resp. infinitary tests with binary results, namely the equivalence of De Nicola and Hennessy resp. the equivalence of ``indiscernibility''. It is shown that indiscernibility is not \(\Pi^ 1_ 1\) and has therefore no complete system of recursive \(\omega\)-proofs, in contrast to De Nicola and Hennessy's equivalence. Section 7 contains an elementary introduction to Girard's work in \(\beta\)-logic showing the existence of complete systems of recursive proofs for indiscernibility and for \(\approx\).
0 references
transition systems
0 references
infinite behaviours
0 references
undecidability
0 references
degrees
0 references
\(\omega\)-behaviours of communicating processes
0 references
logical complexity
0 references
testing equivalences
0 references
proof systems
0 references
infinitary tests
0 references
\(\omega\)-logic
0 references
CCS programs
0 references
indiscernibility
0 references
\(\beta\)-logic
0 references
recursive proofs
0 references