LTL Hierarchies and Model Checking

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

PELÁNEK Radek

Year of publication 2003
Type Article in Proceedings
Conference Proceedings of the Eight ESSLLI Student Session
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords LTL; model checking
Description We propose a new hierarchy of LTL formulas based on alternations of Until and Release operators and show that it is more relevant to model checking then previously studied hierarchies. Moreover, we study practically used formulas and conclude that in most cases it is possible to use specialized algorithms which are more efficient then general algorithm for LTL model checking.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.