Linear temporal logic with until and next, logical consecutions

Тип публикации: статья из журнала

Год издания: 2008

Идентификатор DOI: 10.1016/j.apal.2008.03.001

Ключевые слова: Algorithms, Linear temporal logic, Admissible consecutions, Logical consequence, Admissible inference rules, Admissible consecutions, Admissible inference rules, Algorithms, Linear temporal logic, Logical consequence

Аннотация: While specifications and verifications of concurrent systems employ Linear Temporal Logic (LTL), it is increasingly likely that logical consequence in LTL will be used in the description of computations and parallel reasoning. Our paper considers logical consequence in the standard LTL with temporal operations U (until) and N (next). The prime result is an algorithm recognizing consecutions admissible in LTL, so we prove that LTL is decidable w.r.t. admissible inference rules. As a consequence we obtain algorithms verifying the validity of consecutions in LTL and solving the satisfiability problem. We start by a simple reduction of logical consecutions (inference rules) of LTL to equivalent ones in the reduced normal form (which have uniform structure and consist of formulas of temporal degree 1). Then we apply a semantic technique based on LTL-Kripke structures with formula definable subsets. This yields necessary and sufficient conditions for a consecution to be not admissible in LTL. These conditions lead to an algorithm which recognizes consecutions (rules) admissible in LTL by verifying the validity of consecutions in special finite Kripke structures of size square polynomial in reduced normal forms of the consecutions. As a consequence, this also solves the satisfiability problem for LTL. (C) 2008 Elsevier B.V. All rights reserved.

Ссылки на полный текст



Выпуск журнала: Vol. 155, Is. 1

Номера страниц: 32-45

ISSN журнала: 01680072

Место издания: AMSTERDAM



Вхождение в базы данных

Информация о публикациях загружается с сайта службы поддержки публикационной активности СФУ. Сообщите, если заметили неточности.

Вы можете отметить интересные фрагменты текста, которые будут доступны по уникальной ссылке в адресной строке браузера.