Langanzeige der Metadaten
DC Element | Wert | Sprache |
---|---|---|
dc.contributor.author | Jasper, Marc | - |
dc.contributor.author | Schlüter, Maximilian | - |
dc.contributor.author | Steffen, Bernhard | - |
dc.date.accessioned | 2021-03-05T08:40:38Z | - |
dc.date.available | 2021-03-05T08:40:38Z | - |
dc.date.issued | 2020-05-06 | - |
dc.identifier.uri | http://hdl.handle.net/2003/40062 | - |
dc.identifier.uri | http://dx.doi.org/10.17877/DE290R-21942 | - |
dc.description.abstract | In 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.language.iso | en | de |
dc.relation.ispartofseries | Acta informatica;57(3-5) | - |
dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | - |
dc.subject.ddc | 004 | - |
dc.title | Characteristic invariants in Hennessy-Milner logic | en |
dc.type | Text | de |
dc.type.publicationtype | article | en |
dcterms.accessRights | open access | - |
eldorado.secondarypublication | true | de |
eldorado.secondarypublication.primaryidentifier | https://doi.org/10.1007/s00236-020-00376-5 | de |
eldorado.secondarypublication.primarycitation | Jasper, M., Schlüter, M. & Steffen, B. Characteristic invariants in Hennessy–Milner logic. Acta Informatica 57, 671–687 (2020). | de |
Enthalten in den Sammlungen: | LS 05 Programmiersysteme |
Dateien zu dieser Ressource:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
Jasper2020_Article_CharacteristicInvariantsInHenn.pdf | DNB | 392.65 kB | Adobe PDF | Öffnen/Anzeigen |
Diese Ressource ist urheberrechtlich geschützt. |
Diese Ressource wurde unter folgender Copyright-Bestimmung veröffentlicht: Lizenz von Creative Commons