Show simple item record

dc.contributor.authorNoori-Hosseini, Monaen
dc.contributor.authorLennartson, Bengten
dc.contributor.authorHadjicostis, Christoforosen
dc.creatorNoori-Hosseini, Monaen
dc.creatorLennartson, Bengten
dc.creatorHadjicostis, Christoforosen
dc.date.accessioned2021-01-26T09:46:00Z
dc.date.available2021-01-26T09:46:00Z
dc.date.issued2018
dc.identifier.issn2405-8963
dc.identifier.urihttp://gnosis.library.ucy.ac.cy/handle/7/63498
dc.description.abstractIn this paper, an alternative equivalence based definition of bisimulation is proposed, called visible bisimulation equivalence. It includes both state and transition labels and therefore unifies stuttering and branching bisimulation. Furthermore, it is equivalent to a temporal logic called ECTL*, where CTL* is extended with events. The presented bisimulation abstraction is applied to a set of synchronized submodels, where local events are identified incrementally and abstracted after each synchronization. Since the bisimulation reduction is applied after each synchronization, a significant part of the state space explosion in ordinary synchronization is avoided. This compositional abstraction is used for opacity verification, where it is shown that local observers can be generated before they are synchronized, a key factor to be able to apply compositional opacity verification. The efficiency of this method is illustrated on a modular opacity problem with mutual exclusion of moving agents.en
dc.language.isoenen
dc.sourceIFAC-PapersOnLineen
dc.source.urihttp://www.sciencedirect.com/science/article/pii/S2405896318306670
dc.titleCompositional Visible Bisimulation Abstraction Applied to Opacity Verification ⁎⁎This work was carried out within the project SyTec - Systematic Testing of Cyber-Physical Systems, a Swedish Science Foundation grant for strong research environment. The support is gratefully acknowledged.en
dc.typeinfo:eu-repo/semantics/article
dc.identifier.doi10.1016/j.ifacol.2018.06.337
dc.description.volume51
dc.description.issue7
dc.description.startingpage434
dc.description.endingpage441
dc.author.facultyΠολυτεχνική Σχολή / Faculty of Engineering
dc.author.departmentΤμήμα Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστών / Department of Electrical and Computer Engineering
dc.type.uhtypeArticleen
dc.source.abbreviationIFAC-PapersOnLineen
dc.contributor.orcidHadjicostis, Christoforos [0000-0002-1706-708X]
dc.gnosis.orcid0000-0002-1706-708X


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record