Milner’s complete proof system for observational congruence is crucially based on the possibility to equate τ divergent expressions to non-divergent ones by means of the axiom recX.(τ.X + E) = recX.τ.E. In the presence of a notion of priority, where, e.g., actions of type δ have a lower priority than silent τ actions, this axiom is no longer sound. Such a form of priority is, however, common in timed process algebra, where, due to the interpretation of δ as a time delay, it naturally arises from the maximal progress assumption. We here present our solution, based on introducing an auxiliary operator pri(E) defining a “priority scope”, to the long time open problem of axiomatizing priority using standard observational congruence: we provide a complete axiomatization for a basic process algebra with priority and (unguarded) recursion. We also show that, when the setting is extended by considering static operators of a discrete time calculus, an axiomatization that is complete over (a characterization of) finite-state terms can be developed by re-using techniques devised in the context of a cooperation with Prof. Jos Baeten.

Bravetti M. (2021). Axiomatizing maximal progress and discrete time. LOGICAL METHODS IN COMPUTER SCIENCE, 17(1), 1-44 [10.23638/LMCS-17(1:1)2021].

Axiomatizing maximal progress and discrete time

Bravetti M.
2021

Abstract

Milner’s complete proof system for observational congruence is crucially based on the possibility to equate τ divergent expressions to non-divergent ones by means of the axiom recX.(τ.X + E) = recX.τ.E. In the presence of a notion of priority, where, e.g., actions of type δ have a lower priority than silent τ actions, this axiom is no longer sound. Such a form of priority is, however, common in timed process algebra, where, due to the interpretation of δ as a time delay, it naturally arises from the maximal progress assumption. We here present our solution, based on introducing an auxiliary operator pri(E) defining a “priority scope”, to the long time open problem of axiomatizing priority using standard observational congruence: we provide a complete axiomatization for a basic process algebra with priority and (unguarded) recursion. We also show that, when the setting is extended by considering static operators of a discrete time calculus, an axiomatization that is complete over (a characterization of) finite-state terms can be developed by re-using techniques devised in the context of a cooperation with Prof. Jos Baeten.
2021
Bravetti M. (2021). Axiomatizing maximal progress and discrete time. LOGICAL METHODS IN COMPUTER SCIENCE, 17(1), 1-44 [10.23638/LMCS-17(1:1)2021].
Bravetti M.
File in questo prodotto:
File Dimensione Formato  
2001.08040.pdf

accesso aperto

Tipo: Versione (PDF) editoriale
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione 557.4 kB
Formato Adobe PDF
557.4 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/815638
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact