Verify LTL with Fairness Assumptions Efficiently

Li, Y; Song, L; Feng, Y; Zhang, L

Verify LTL with Fairness Assumptions Efficiently

Li, Y Song, L Feng, Y

Zhang, L

Permalink

Publication Type:: Conference Proceeding
Citation:: Proceedings of the International Workshop on Temporal Representation and Reasoning, 2016, 2016-December pp. 41 - 50
Issue Date:: 2016-12-05

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Accepted ManuscriptAdobe PDF (263.73 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Li, Y	en_US
dc.contributor.author	Song, L	en_US
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896	en_US
dc.contributor.author	Zhang, L	en_US
dc.date.issued	2016-12-05	en_US
dc.identifier.citation	Proceedings of the International Workshop on Temporal Representation and Reasoning, 2016, 2016-December pp. 41 - 50	en_US
dc.identifier.isbn	9781509038251	en_US
dc.identifier.uri	http://hdl.handle.net/10453/101742
dc.description.abstract	© 2016 IEEE. This paper deals with model checking problems with respect to LTL properties under fairness assumptions. We first present an efficient algorithm to deal with a fragment of fairness assumptions and then extend the algorithm to handle arbitrary ones. Notably, by making use of some syntactic transformations, our algorithm avoids constructing corresponding Büchi automata for the whole fairness assumptions, which can be very large in practice. We implement our algorithm in NuSMV and consider a large selection of formulas. Our experiments show that in many cases our approach exceeds the automata-theoretic approach up to several orders of magnitude, in both time and memory.	en_US
dc.relation.ispartof	Proceedings of the International Workshop on Temporal Representation and Reasoning	en_US
dc.relation.isbasedon	10.1109/TIME.2016.12	en_US
dc.title	Verify LTL with Fairness Assumptions Efficiently	en_US
dc.type	Conference Proceeding
utslib.citation.volume	2016-December	en_US
utslib.for	080203 Computational Logic and Formal Languages	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	open_access
pubs.publication-status	Published	en_US
pubs.volume	2016-December	en_US

Abstract:

© 2016 IEEE. This paper deals with model checking problems with respect to LTL properties under fairness assumptions. We first present an efficient algorithm to deal with a fragment of fairness assumptions and then extend the algorithm to handle arbitrary ones. Notably, by making use of some syntactic transformations, our algorithm avoids constructing corresponding Büchi automata for the whole fairness assumptions, which can be very large in practice. We implement our algorithm in NuSMV and consider a large selection of formulas. Our experiments show that in many cases our approach exceeds the automata-theoretic approach up to several orders of magnitude, in both time and memory.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/101742