Show simple item record  

dc.contributor.authorWare, Simon
dc.contributor.authorMalik, Robi
dc.date.accessioned2012-06-05T03:53:26Z
dc.date.available2013-10-31T19:50:33Z
dc.date.copyright2012-03-25
dc.date.issued2012
dc.identifier.citationWare, S. & Malik, R. (2012). Conflict-preserving abstraction of discrete event systems using annotated automata. Discrete Event Dynamic Systems, 22(4), 451-477.en_NZ
dc.identifier.urihttps://hdl.handle.net/10289/6387
dc.description.abstractThis paper proposes to enhance compositional verification of the nonblocking property of discrete event systems by introducing annotated automata. Annotations store nondeterministic branching information, which would otherwise be stored in extra states and transitions. This succinct representation makes it easier to simplify automata and enables new efficientmeans of abstraction, reducing the size of automata to be composed and thus the size of the synchronous product state space encountered in verification. The abstractions proposed are of polynomial complexity, and they have been successfully applied to model check the nonblocking property of the same set of large-scale industrial examples as used in related work.en_NZ
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherSpringeren_NZ
dc.relation.ispartofDiscrete Event Dynamic Systems
dc.relation.urihttp://www.springerlink.com/content/n745411320882t75/en_NZ
dc.rightsThis is an author’s accepted version of an article published in the journal: Discrete Event Dynamic Systems. © 2012 Springer.
dc.subjectcomputer scienceen_NZ
dc.subjectdiscrete event systemsen_NZ
dc.subjectfinite state machinesen_NZ
dc.subjectmodel checkingen_NZ
dc.subjectnonblockingen_NZ
dc.titleConflict-preserving abstraction of discrete event systems using annotated automataen_NZ
dc.typeJournal Articleen_NZ
dc.identifier.doi10.1007/s10626-012-0133-3en_NZ
dc.relation.isPartOfDiscrete Event Dynamic Systemsen_NZ
pubs.begin-page451en_NZ
pubs.elements-id37407
pubs.end-page477en_NZ
pubs.issue4en_NZ
pubs.volume22en_NZ


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record