We refine Alex Simpson's approach to formal verification of properties of concurrent systems via proof systems. Our new sequent calculus G3HMLGSOS seamlessly harmonises the GSOS semantics for process calculi (for system formalisation) with Hennessy-Milner logic (for formal property specification) in a pure G3-style system, from which the cut-rule is efectively eliminated. We achieve this substantial improvement by applying the geometrisation of formal theories introduced in the proof-theoretic literature by Roy Dyckhof and Sara Negri. We communicate here our design methodology to fine-tune Simpson's calculi, which we consider promising to cover, in the future, more expressive process algebra's specification formalisms and logics in a principled and uniform manner.
It is well-known that computational/behavioural equivalence of concurrent processes can
be logically characterised by (possibly variants and extensions of) Hennessy-Milner modal
systems [
In his [
Stirling partially achieved such a proof system for CCS at the price of breaking the analyticity of the calculus in order to handle restriction and parallel composition operators. The methodology proposed in that seminal paper thus generated calculi that are not structurally complete. As a practical consequence, verification of process properties through proof-search cannot be automated even for recursion-free CCS.
Years later, in [
In particular, the paper [
First, the availability of a cut rule is crucial for implementing a formal verification that
satisfies most of these desiderata and is also modular or compositional in the original sense first
envisaged by Stirling in [
In his original papers, Simpson provides a semantic proof of cut admissibility – i.e. he derives the technical contents of Requirement (6) from Requirement (5) – in a labelled sequent calculus for Hennessy-Milner logic specifying properties of GSOS processes.
We think we can obtain more general results – covering more general process formalisms and more expressive modal logics for processes – by a more principled proof system design methodology that refines Simpson’s calculi and builds on recent advances in structural proof theory.
More precisely, we propose diferent sequent rules for process operators , based on the
geometrisation methods discussed in detail by Roy Dyckhof and Sara Negri [ 14]. We use them to define
a new G3-style labelled sequent calculus, that we named G3HMLGSOS, targeting the same class of
processes and logic as Simpson’s work, i.e. Hennessy-Milner logic [
Our main technical advancement in this proof-theoretic approach to process verification is
the constructive proof of structural completeness of the calculus. More relevantly, we provide a
cut-elimination algorithm for G3HMLGSOS(Theorem 1), which is an essential first result towards
implementing the compositional verification initially discussed by Stirling in [
In other terms, by adopting our calculus design method, we provide a direct and constructive proof of Requirement (4) (analyticity) without compromising Requirement (6) (compositionality), still making Requirements (2-3) hold by design (ordinary and parametrised verification). Requirement (1) (soundness) is then straightforward to prove,1 and Requirements (5) and (7) (semantic completeness, and termination of proof-search for the expected fragments of GSOS, resp.) are proven by Tait-Schütte-Takeuti saturation method.2
It is a first but relevant and promising fine-tuning of Simpson’s original answer to Stirling’s
research question. The results we communicate here may prelude to further extensions for
more expressive logics (such as those proposed in [
In the following pages, we overview and discuss our design choices for G3HMLGSOS, focusing on the main diference from Simpson’s calculi – i.e. sequent rules for GSOS process – which enables us to define a pure G3-style calculus using only rules that directly express the logical connectives and process operators, for which we can directly prove cut-elimination and structural completeness.
We borrow from the process algebra literature some notations and formal definitions concerning
signatures, process terms, labelled transition systems (LTS), and transition system
specifications (TSS): we refer the reader to e.g. [
(⋆) { → | 1 ≤ ≤ , 1 ≤ ≤ }
∪ (⃗) → (⃗, ⃗) where the ’s and the ’s (1 ≤ ≤ and 1 ≤ ≤ ) are all distinct process variables; , and ℓ are natural numbers; (⃗, ⃗) is a process term with variables including at most the { ̸→ | 1 ≤ ≤ , 1 ≤ ≤ ℓ} 1See the proof techniques discussed in [17]. 2See [18] and [19]. ’s and ’s; and the ’s, ’s and are actions from . We call any expression of the form → ′ a positive relational atom – formalising the fact that process evolves through action into process ′ – and any expression of the form ̸ → a negative relational atom – formalising the fact that process does not evolve into any process through action – where , ′ are process terms.3
We are ready to define the syntax of our proof system G3HMLGSOS.
Definition 1. Structural atoms are positive relational atoms, negative relational atoms, or atoms of shape ≡ , where ∈ and ≡ denotes a given congruence relation (possibly, syntactic equality) between process terms.
Labelled formulas are either structural atoms or formulas of shape : (read as “formula is forced by process ”), where is a formula in Hennessy-Milner logic and is a process term. We denote by a generic labelled formula.
Sequents of G3HMLGSOS are expressions Γ ⇒ Δ, where Γ, Δ are finite multisets of labelled formulas, and structural atoms may occur only in Γ.
Logical rules. The logical rules are the multimodal version of the standard rules for G3K [17], based on the semantic clauses for local forcing relation of Hennessy-Milner formulas on a given labelled transition system. We omit the standard rules for classical propositional connectives, to recall only the modal rules: : , → , : [ ], Γ ⇒ Δ → , : [ ], Γ ⇒ Δ □ → , Γ ⇒ Δ, : □ (!) Γ ⇒ Δ, : [ ] The rule □ corresponds to the right-to-left direction of the definition of local forcing for [ ]: the side condition (!) denotes the requirement on not to occur in Γ, Δ; in this situation, is said the eigenvariable of the rule. The rule □ corresponds to the left-to-right direction of the same definition of local forcing. Notice that this is a first diference from the system introduced by Simpson, as, contrary to his system, we can handle modal operators keeping structural atoms only on the left-hand side of sequents.
⋀︀
1≤ ≤ ,1≤ ≤
Compositional rules. For each process operator, we need to introduce in G3HMLGSOS some
rules characterising it in terms of the associated GSOS specification. We notice first that each of
these rules can be translated into geometric formulas. In fact, any GSOS rule of shape (⋆) above
states at the meta-level that the following formulas (∘ ) and (∘ ) hold:
(∘ ) ∀⃗, ⃗ : [︃(︃ ( → ) & ( ̸ → ))︃ ⊃ ( (⃗) → (⃗, ⃗))]︃
⋀︀
1≤ ≤ ,1≤ ≤ ℓ
3A GSOS specification system naturally defines an LTS over the closed terms of a signature by structural induction.
Refer to, e.g., [
[︃
︃( (∘ ) ∀⃗, ⃗, : ( (⃗) → ) ⊃ ∃⃗ : (⃗, ⃗) ≡ &
⋀︀ 1≤ ≤ ,1≤ ≤ ( → ) &
⋀︀ 1≤ ≤ ,1≤ ≤ ℓ ( ̸ → ) )︃]︃
These formulas become geometric by adopting the “semidefinitional extension trick” of [ 14] to turn the generic negative relational atom ̸ → into ∀ : ( → ⊃ ⊥ methodology of [17, 14], we can then introduce the following rules of our G3HMLGSOS for the ). Following the GSOS specification of processes 4 ̸ → , → , Γ ⇒ Δ ̸ → Def (⃗) → , Γ ⇒ Δ Atm(), Atm(), ≡ , Γ ⇒ Δ
Atm(), ≡ , Γ ⇒ Δ
Repl1
Atm(), Atm(), ≡ , Γ ⇒ Δ
Atm(), ≡ , Γ ⇒ Δ
Repl2 (eigenvariable condition).
In the replacement rules, Atm() stands for → , or → , or ̸ → , or ≡ rule ∘ ∘ , is the number of GSOS rules in the TSS for the operator and action ; the side condition (!⃗) denotes the requirement on ’s not to occur in the conclusion of ∘ ∘ . In the
These rules mark the main diference from Simpson’s original calculus [12, p. 301], as we are, once again, able to handle process operators by keeping structural atoms only on the left-hand side of sequents, so that we can dismiss all the additional non-logical rules of [12, Fig. 4], proving straightforwardly the structural completeness of our G3HMLGSOS.
More relevantly, contrary to what happens for Simpson’s system, we can give a direct and constructive proof of cut-elimination by standard double induction:5
The rule of cut Γ ⇒ Δ, :
: , Γ′ ⇒ Δ′ Γ, Γ′ ⇒ Δ, Δ′
Cut (where : is called the cut formula of the rule) is admissible in G3HMLGSOS . 4For some operators, further rules (omitted here) should be added to deal with those instances presenting a duplication of the atoms in the conclusion in order to have contraction rules height-preserving admissible. We refer the reader to [17] for an extensive discussion. 5From cut admissibility, we easily derive: admissibility of generalised replacement rules; axiomatic completeness w.r.t Hennessy-Milner logic; (semantic) -completeness via Tait-Schütte-Takeuti saturation method.
This work was partially funded by: the project SERICS – Security and Rights in CyberSpace PE0000014, financed within PNRR, M4C2 I.1.3, funded by the European Union - NextGenerationEU (MUR Code: 2022CY2J5S); the MIUR project PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems); Istituto Nazionale di Alta Matematica – INdAM group GNSAGA.
We thank three anonymous referees for their comments and feedback on the first submission. arbitrary GSOS, J. Log. Algebraic Methods Program. 60-61 (2004) 287–322. URL: https: //doi.org/10.1016/j.jlap.2004.03.004. doi:10.1016/J.JLAP.2004.03.004. [13] B. Bloom, S. Istrail, A. R. Meyer, Bisimulation can’t be traced, J. ACM 42 (1995) 232–268.
URL: https://doi.org/10.1145/200836.200876. doi:10.1145/200836.200876. [14] R. Dyckhof, S. Negri, Geometrisation of first-order logic, Bull. Symb. Log. 21 (2015) 123–163. URL: https://doi.org/10.1017/bsl.2015.7. doi:10.1017/BSL.2015.7. [15] C. Stirling, A proof system with names for modal mu-calculus, in: A. Banerjee, O. Danvy, K. Doh, J. Hatclif (Eds.), Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, Manhattan, Kansas, USA, 19-20th September 2013, volume 129 of EPTCS, 2013, pp. 18–29. URL: https: //doi.org/10.4204/EPTCS.129.2. doi:10.4204/EPTCS.129.2. [16] C. Stirling, A tableau proof system with names for modal mu-calculus, in: A. Voronkov, M. V. Korovina (Eds.), HOWARD-60: A Festschrift on the Occasion of Howard Barringer’s 60th Birthday, volume 42 of EPiC Series in Computing, EasyChair, 2014, pp. 306–318. URL: https://doi.org/10.29007/lwqm. doi:10.29007/lwqm. [17] S. Negri, J. Von Plato, Proof analysis: a contribution to Hilbert’s last problem, Cambridge
University Press, 2011. [18] A. S. Troelstra, H. Schwichtenberg, Basic proof theory, Second Edition, volume 43 of
Cambridge tracts in theoretical computer science, Cambridge University Press, 2000. [19] A. Indrzejczak, Sequents and trees, Studies in Universal Logic, Birkhäuser, Cham (2021). [20] R. De Nicola, M. Loreti, A modal logic for mobile agents, ACM Trans. Comput. Log. 5 (2004) 79–128. URL: https://doi.org/10.1145/963927.963930. doi:10.1145/963927.963930. [21] B. Afshari, L. Grotenhuis, G. E. Leigh, L. Zenger, Ill-founded proof systems for intuitionistic linear-time temporal logic, in: R. Ramanayake, J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings, volume 14278 of Lecture Notes in Computer Science, Springer, 2023, pp. 223–241. URL: https://doi.org/10. 1007/978-3-031-43513-3_13. doi:10.1007/978-3-031-43513-3\_13. [22] B. Afshari, G. E. Leigh, G. M. Turata, A cyclic proof system for full computation tree logic, in: B. Klin, E. Pimentel (Eds.), 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, volume 252 of LIPIcs, Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2023, pp. 5:1–5:19. URL: https://doi.org/10.4230/LIPIcs.
CSL.2023.5. doi:10.4230/LIPICS.CSL.2023.5. [23] B. Afshari, G. E. Leigh, G. M. Turata, Demystifying , CoRR abs/2401.01096 (2024). URL: https://doi.org/10.48550/arXiv.2401.01096. doi:10.48550/ARXIV.2401. 01096. arXiv:2401.01096. [24] B. Afshari, S. Enqvist, G. E. Leigh, Cyclic proofs for the first-order -calculus, Log. J. IGPL 32 (2024) 1–34. URL: https://doi.org/10.1093/jigpal/jzac053. doi:10.1093/JIGPAL/JZAC053. [25] M. Maggesi, C. Perini Brogi, A formal proof of modal completeness for provability logic, in: L. Cohen, C. Kaliszyk (Eds.), 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, pp. 26:1–26:18. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.26. doi:10.4230/LIPICS.ITP.2021.26. [26] M. Maggesi, C. Perini Brogi, Mechanising Gödel-Löb provability logic in HOL light, J.
Autom. Reason. 67 (2023) 29. URL: https://doi.org/10.1007/s10817-023-09677-z. doi:10. 1007/S10817-023-09677-Z. [27] L. Viganò, Labelled non-classical logics, Springer Science & Business Media, 2013. [28] A. K. Simpson, The proof theory and semantics of intuitionistic modal logic, University of Edinburgh. College of Science and Engineering. (1994).