Proof systems for infinite behaviours

DOI10.1016/0890-5401(92)90029-FMaRDI QIDQ1193598zbMATH OpenFDO

Authors Philippe Darondeau, Serge Yoccoz

Publication date 27 September 1992

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0890-5401(92)90029-F

zbMATH Keywords

\(\beta\)-logic\(\omega\)-behaviours of communicating processes\(\omega\)-logicCCS programsdegreesindiscernibilityinfinitary testsinfinite behaviourslogical complexityproof systemsrecursive proofstesting equivalencestransition systemsundecidability

Mathematics Subject Classification ID

Logic in computer science (03B70) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10)

Review text

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\).

Recommendations

• Testing equivalences for processes
• Proof systems for message-passing process algebras
• CCS expressions, finite state processes, and three problems of equivalence
• Complete proof systems for observation congruences in finite-control -calculus
• scientific article; zbMATH DE number 3928330

Cites work

• A calculus of communicating systems
• Descriptive set theory
• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 3556029 (Why is no real title available?)
• scientific article; zbMATH DE number 3572138 (Why is no real title available?)
• scientific article; zbMATH DE number 3995044 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• Recursive \(\omega\)-rule for proof systems
• Refusal testing
• Second order arithmetic and related topics
• Synchronous and asynchronous experiments on processes
• Testing equivalences for processes
• Une critique de la notion de test de processus fondée sur la non séparabilité de certaines classes de langages
• Π12-logic, Part 1: Dilators

Cited in

(9)

• On an effective hierarchy of communicating processes: Separation principle and testing
• scientific article; zbMATH DE number 4199644 (Why is no real title available?)
• Highly Undecidable Problems For Infinite Computations
• scientific article; zbMATH DE number 3600027 (Why is no real title available?)
• scientific article; zbMATH DE number 1534491 (Why is no real title available?)
• Proving infinitary formulas
• scientific article; zbMATH DE number 7238899 (Why is no real title available?)
• An equational characterisation of the must testing pre-order for regular processes
• On the logic of UNITY

This page was built for publication: Proof systems for infinite behaviours

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1193598)