[en] Since the topic emerged several years ago, work on regular model checking has mostly been devoted to the verification of state reachability and safety properties. Though it was known that liveness properties could also be checked within this framework, little has been done about working out the corresponding details, and experimentally evaluating the approach. This paper addresses these issues in the context of regular model checking based on the encoding of states by finite or infinite words. It works out the exact constructions to be used in both cases, and solves the problem resulting from the fact that infinite computations of unbounded configurations might never contain the same configuration twice, thus making cycle detection problematic. Several experiments showing the applicability of the approach were successfully conducted.
Disciplines :
Computer science
Author, co-author :
Bouajjani, Ahmed; University of Paris 7, LIAFA
Legay, Axel ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
Language :
English
Title :
Handling Liveness Properties in (ω-)Regular Model Checking
Publication date :
28 December 2005
Event name :
6th International Workshop on Verification of Infinite-State Systems
Event place :
Londres, United Kingdom
Event date :
4 septembre 2004
Audience :
International
Journal title :
Electronic Notes in Theoretical Computer Science
eISSN :
1571-0661
Publisher :
Elsevier, Amsterdam, Netherlands
Special issue title :
Proceedings of the 6th International Workshop on Verification of Infinite-State Systems (INFINITY 2004)
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.
Bibliography
P.A. Abdulla and B. Jonsson and M. Nilsson and J. d'Orso and M. Saksena, Regular Model Checking for S1S + LTL
A. Bouajjani, A. Collomb-Annichini, Y. Lakhnech, and M. Sighireanu Analyzing Fair Parametric Extended Automata Lecture Notes in Computer Science volume 2126 2001
A. Bouajjani, B. Jonsson, M. Nilsson, and Tayssir Touili Regular Model Checking Proceedings of the 12th International Conference on Computer-Aided Verification (CAV'00) Lecture Notes in Computer Science volume 1855 2000 403 418
B. Boigelot and S. Jodogne and P. Wolper", On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables, Proc. International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Computer Science, volume 2083, year 200, pages 611-625
B. Boigelot, A. Legay, and P. Wolper Iterating Transducers in the Large Proc. 15th Int. Conf. on Computer Aided Verification, Boulder, USA Lecture Notes in Computer Science volume 2725 2003 223 235
B. Boigelot, A. Legay, and P. Wolper Omega-Regular Model Checking Proc. 10th Int. Conf. on Tools and techniques, Barcelona, Spain Lecture Notes in Computer Science volume 2988 2004 561 575
Y. Fang and N. Piterman and A. Pnueli and L. Zuck, Liveness with Incomprehensible Ranking, Proc. 10th Int. Conf. on Tools and techniques, Barcelona, Spain, Lecture Notes in Computer Science, volume 2988, year, pages 482-496
K. Baukus, Y. Lakhnech, and K. Stahl Verifying Universal Properties of Parametrized Networks FTRTFT'00 Lecture Notes in Computer Science volume 1926 2000
D. Dams, Y. Lakhnech, and M. Steffen Iterating Transducers Proceedings 13th International Conference on Computer Aided Verification (CAV) Lecture Notes in Computer Science volume 2102 2001 286 297
M.Y. Vardi, and P. Wolper Automata-Theoretic Techniques for Modal Logics of Programs Journal of Computer and System Science 32 2 1986 183 221
M. Colon, and H. Sipma Practical Methods for Proving Program Termination Proc. 14th Int. Conf. on Computer Aided Verification, Copenhagen, Denmark Lecture Notes in Computer Science volume 2404 2002 442 454
D. Dams and R. Gerth and O. Grumberg, A heuristic for the automatic generation of ranking functions, Proceedings of WAVe00, URL: citeseer.nj.nec.com/article/dams00heuristic.html
A. Bouajjani and A. Legay and P. Wolper, Handling Liveness Properties in (ω-)Regular Model Checking: full version, Technical Report, URL: http://www.montefiore.ulg.ac.be/legay/WWW/papers/infinity04.ps
Y. Kesten and O. Maler and M. Marcus and A. Pnueli and E. Shahar, Symbolic Model Checking with Rich Assertional Languages, Proceedings of 9th International Conference on Computer-Aided Verification (CAV'97), Lecture Notes in Computer Science, volume 1254
D.E. Muller and A. Saoudi and P.E. Schupp, Alternating automata, the weak monadic theory of the tree and its complexity, Proc. 13th Int. Colloquium on Automata, Languages and Programming, year 1986
A. Pnueli, and E. Shahar Liveness and Acceleration in Parameterized Verification Proceedings of the 12th International Conference on Computer-Aided Verification (CAV'00) Lecture Notes in Computer Science volume 1855 2000 328 343
A. Pnueli, J. Xu, and L. Zuck Liveness with (0,1,infinite)-Counter Abstraction Proc. 14th Int. Conf. on Computer Aided Verification, Copenhagen, Denmark Lecture Notes in Computer Science volume 2404 2002 107 122
Similar publications
Sorry the service is unavailable at the moment. Please try again later.
This website uses cookies to improve user experience. Read more
Save & Close
Accept all
Decline all
Show detailsHide details
Cookie declaration
About cookies
Strictly necessary
Performance
Strictly necessary cookies allow core website functionality such as user login and account management. The website cannot be used properly without strictly necessary cookies.
This cookie is used by Cookie-Script.com service to remember visitor cookie consent preferences. It is necessary for Cookie-Script.com cookie banner to work properly.
Performance cookies are used to see how visitors use the website, eg. analytics cookies. Those cookies cannot be used to directly identify a certain visitor.
Used to store the attribution information, the referrer initially used to visit the website
Cookies are small text files that are placed on your computer by websites that you visit. Websites use cookies to help users navigate efficiently and perform certain functions. Cookies that are required for the website to operate properly are allowed to be set without your permission. All other cookies need to be approved before they can be set in the browser.
You can change your consent to cookie usage at any time on our Privacy Policy page.