Characteristic invariants in Hennessy-Milner logic

Simple item page
dc.contributor.authorJasper, Marc
dc.contributor.authorSchlüter, Maximilian
dc.contributor.authorSteffen, Bernhard
dc.date.accessioned2021-03-05T08:40:38Z
dc.date.available2021-03-05T08:40:38Z
dc.date.issued2020-05-06
dc.description.abstractIn this paper, we prove that Hennessy–Milner Logic (HML), despite its structural limitations, is sufficiently expressive to specify an initial property φ0 and a characteristic invariant χI for an arbitrary finite-state process P such that φ0∧AG(χI) is a characteristic formula for P. This means that a process Q, even if infinite state, is bisimulation equivalent to P iff Q⊨φ0∧AG(χI). It follows, in particular, that it is sufficient to check an HML formula for each state of a finite-state process to verify that it is bisimulation equivalent to P. In addition, more complex systems such as context-free processes can be checked for bisimulation equivalence with P using corresponding model checking algorithms. Our characteristic invariant is based on so called class-distinguishing formulas that identify bisimulation equivalence classes in P and which are expressed in HML. We extend Kanellakis and Smolka’s partition refinement algorithm for bisimulation checking in order to generate concise class-distinguishing formulas for finite-state processes.en
dc.identifier.urihttp://hdl.handle.net/2003/40062
dc.identifier.urihttp://dx.doi.org/10.17877/DE290R-21942
dc.language.isoende
dc.relation.ispartofseriesActa informatica;57(3-5)
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.subject.ddc004
dc.titleCharacteristic invariants in Hennessy-Milner logicen
dc.typeTextde
dc.type.publicationtypearticleen
dcterms.accessRightsopen access
eldorado.secondarypublicationtruede
eldorado.secondarypublication.primarycitationJasper, M., Schlüter, M. & Steffen, B. Characteristic invariants in Hennessy–Milner logic. Acta Informatica 57, 671–687 (2020).de
eldorado.secondarypublication.primaryidentifierhttps://doi.org/10.1007/s00236-020-00376-5de

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Jasper2020_Article_CharacteristicInvariantsInHenn.pdf
Size:
392.65 KB
Format:
Adobe Portable Document Format
Description:
DNB
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
4.85 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

LS 05 Programmiersysteme