Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps

Benjamin Bisping; David N. Jansen

Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2305.17671 v3 pith:TSFNZ6JM submitted 2023-05-28 cs.LO cs.GT

Benjamin Bisping , David N. Jansen This is my paper · ORCID

classification cs.LOcs.GT

keywords characterizeenergygamelinear-time--branching-timesilentstepsweakaccounting

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

read the original abstract

We provide the first generalized game characterization of van Glabbeek's linear-time--branching-time spectrum with silent steps. Thereby, one multi-dimensional energy game can be used to characterize and decide a wide array of weak behavioral equivalences between stability-respecting branching bisimilarity and weak trace equivalence in one go. To establish correctness, we relate attacker-winning energy budgets and distinguishing sublanguages of Hennessy--Milner logic that we characterize by eight dimensions of formula expressiveness.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics
cs.LO 2024-11 conditional novelty 7.0 of 10

A single generalized energy game characterizes and decides the silent-step behavioral equivalence spectrum between branching bisimilarity and weak trace semantics.

Pith tools