Mario Bravetti - Axiomatizing Maximal Progress and Discrete Time

lmcs:6048 - Logical Methods in Computer Science, January 21, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:1)2021
Axiomatizing Maximal Progress and Discrete TimeArticle

Authors: Mario Bravetti

    Milner's complete proof system for observational congruence is crucially based on the possibility to equate $\tau$ divergent expressions to non-divergent ones by means of the axiom $recX. (\tau.X + E) = recX. \tau. E$. In the presence of a notion of priority, where, e.g., actions of type $\delta$ have a lower priority than silent $\tau$ 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 $\delta$ 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.


    Volume: Volume 17, Issue 1
    Published on: January 21, 2021
    Accepted on: October 20, 2020
    Submitted on: January 23, 2020
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages
    Funding:
      Source : OpenAIRE Graph
    • Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233

    Consultation statistics

    This page has been seen 1583 times.
    This article's PDF has been downloaded 249 times.