Skip to Main content Skip to Navigation
Journal articles

Axiomatizing Maximal Progress and Discrete Time

Mario Bravetti 1, 2 
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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. Research partly supported by the H2020-MSCA-RISE project ID 778233 "Behavioural Application Program Interfaces (BEHAPI)".
Document type :
Journal articles
Complete list of metadata
Contributor : Mario Bravetti Connect in order to contact the contributor
Submitted on : Friday, September 10, 2021 - 11:55:52 AM
Last modification on : Friday, July 8, 2022 - 10:04:22 AM


Files produced by the author(s)




Mario Bravetti. Axiomatizing Maximal Progress and Discrete Time. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2021, ⟨10.23638/LMCS-17(1:1)2021⟩. ⟨hal-03340630⟩



Record views


Files downloads