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

https://hal.inria.fr/hal-03340630
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

File

lmcs1.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

12

Files downloads

18