Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications

Simple item page
dc.contributor.authorMohajerani, Saharen_NZ
dc.contributor.authorMalik, Robien_NZ
dc.contributor.authorWintenberg, Andrewen_NZ
dc.contributor.authorLafortune, Stephaneen_NZ
dc.contributor.authorOzay, Necmiyeen_NZ
dc.date.accessioned2021-06-08T22:09:57Z
dc.date.available2021-06-08T22:09:57Z
dc.date.issued2021en_NZ
dc.description.abstractThis paper proposes a method to synthesise controllers for systems with possibly infinite number of states that satisfy a specification given as an LTL\◦ formula. A common approach to handle this problem is to first compute a finite-state abstraction of the original state space and then synthesise a controller for the abstraction. This paper proposes to use an abstraction method called divergent stutter bisimulation to abstract the state space of the system. As divergent stutter bisimulation factors out stuttering steps, it typically results in a coarser and therefore smaller abstraction, at the expense of not preserving the temporal ‘‘next’’ operator. The paper leverages results about divergent stutter bisimulation from model checking and shows that divergent stutter bisimulation is a sound and complete abstraction method when synthesising controllers subject to specifications in LTL\◦.
dc.format.mimetypeapplication/pdf
dc.identifier.citationMohajerani, S., Malik, R., Wintenberg, A., Lafortune, S., & Ozay, N. (2021). Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications. Automatica, 130, 109723–109723. https://doi.org/10.1016/j.automatica.2021.109723en
dc.identifier.doi10.1016/j.automatica.2021.109723en_NZ
dc.identifier.issn0005-1098en_NZ
dc.identifier.urihttps://hdl.handle.net/10289/14366
dc.language.isoenen_NZ
dc.publisherElsevier BVen_NZ
dc.relation.isPartOfAutomaticaen_NZ
dc.rights© 2021 The Author(s). Published by Elsevier Ltd. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).
dc.subjectcomputer scienceen_NZ
dc.subjectcontrol synthesisen_NZ
dc.subjectcomputational issuesen_NZ
dc.subjectcontroller constraints and structureen_NZ
dc.subjectAbstractionen_NZ
dc.subjectspecificationen_NZ
dc.titleDivergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specificationsen_NZ
dc.typeJournal Article
pubs.begin-page109723
pubs.elements-id261631
pubs.end-page109723
pubs.organisational-group/Waikato
pubs.organisational-group/Waikato/2025 PBRF
pubs.organisational-group/Waikato/DHECS
pubs.organisational-group/Waikato/DHECS/2025 PBRF - DHEC
pubs.organisational-group/Waikato/DHECS/SCMS
pubs.organisational-group/Waikato/DHECS/SCMS/2025 PBRF - SCMS
pubs.publication-statusAccepteden_NZ
pubs.user.infoMalik, Khalid (robi@waikato.ac.nz)
pubs.volume130en_NZ
uow.identifier.article-no109723
uow.verification.statusverified
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
1-s2.0-S0005109821002430-main.pdf
Size:
990.58 KB
Format:
Adobe Portable Document Format
Description:
Published version
Thumbnail Image
Name: 1-s2.0-S0005109821002430-main.pdf
Size: 990.58 KB
Kind: Adobe PDF
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
Research Commons Deposit Agreement 2017.pdf
Size:
188.11 KB
Format:
Adobe Portable Document Format
Description:
Name: Research Commons Deposit Agreement 2017.pdf
Size: 188.11 KB
Kind: Adobe PDF
Collections
Computing and Mathematical Sciences Papers