Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages - Laboratoire Méthodes Formelles Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages

Résumé

One of the main motivations for this work is to obtain a distributed Krohn-Rhodes theorem for Mazurkiewicz traces. Concretely, we focus on the recently introduced operation of local cascade product of asynchronous automata and ask if every regular trace language can be accepted by a local cascade product of "simple" asynchronous automata. Our approach crucially relies on the development of a local and past-oriented propositional dynamic logic (LocPastPDL) over traces which is shown to be expressively complete with respect to all regular trace languages. An event-formula of LocPastPDL allows to reason about the causal past of an event and a path-formula of LocPastPDL, localized at a process, allows to march along the sequence of past-events in which that process participates, checking for local regular patterns interspersed with local tests of other event-formulas. We also use additional constant formulas to compare the leading process events from the causal past. The new logic LocPastPDL is of independent interest, and the proof of its expressive completeness is rather subtle. Finally, we provide a translation of LocPastPDL formulas into local cascade products. More precisely, we show that every LocPastPDL formula can be computed by a restricted local cascade product of the gossip automaton and localized 2-state asynchronous reset automata and localized asynchronous permutation automata.
Fichier principal
Vignette du fichier
2022-09 CONCUR.pdf (768.45 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

hal-03770358 , version 1 (06-09-2022)

Identifiants

Citer

Bharat Adsul, Paul Gastin, Saptarshi Sarkar, Pascal Weil. Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages. 33rd International Conference on Concurrency Theory (CONCUR 2022), Sep 2022, Warszawa, Poland. pp.28:1-28:19, ⟨10.4230/LIPIcs.CONCUR.2022.28⟩. ⟨hal-03770358⟩
68 Consultations
45 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More