Proof systems for infinite behaviours (Q1193598): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
ReferenceBot (talk | contribs) Changed an Item |
||
(One intermediate revision by one other user not shown) | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Second order arithmetic and related topics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Une critique de la notion de test de processus fondée sur la non séparabilité de certaines classes de langages / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4721642 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Testing equivalences for processes / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3773876 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4128539 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Π12-logic, Part 1: Dilators / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Synchronous and asynchronous experiments on processes / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A calculus of communicating systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5322161 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3907077 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Refusal testing / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5573961 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4143283 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Recursive \(\omega\)-rule for proof systems / rank | |||
Normal rank |
Latest revision as of 14:19, 16 May 2024
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
0 references