REASONING ABOUT BOUNDED TIME DOMAIN - An Alternative to NP-Complete Fragments of LTL

Norihiro Kamide

2010

Abstract

It is known that linear-time temporal logic (LTL) is one of the most useful logics for reasoning about time and for verifying concurrent systems. It is also known that the satisfiability problem for LTL is PSPACE-complete and that finding NP-complete fragments of LTL is an important issue for constructing efficiently executable temporal logics. In this paper, an alternative NP-complete logic called bounded linear-time temporal logic is obtained from LTL by restricting the time domain of temporal operators.

Paper Citation

in Harvard Style

Kamide N. (2010). REASONING ABOUT BOUNDED TIME DOMAIN - An Alternative to NP-Complete Fragments of LTL . In Proceedings of the 2nd International Conference on Agents and Artificial Intelligence - Volume 1: ICAART, ISBN 978-989-674-021-4, pages 536-539. DOI: 10.5220/0002714805360539

in Bibtex Style

@conference{icaart10,
author={Norihiro Kamide},
title={REASONING ABOUT BOUNDED TIME DOMAIN - An Alternative to NP-Complete Fragments of LTL},
booktitle={Proceedings of the 2nd International Conference on Agents and Artificial Intelligence - Volume 1: ICAART,},
year={2010},
pages={536-539},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0002714805360539},
isbn={978-989-674-021-4},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 2nd International Conference on Agents and Artificial Intelligence - Volume 1: ICAART,
TI - REASONING ABOUT BOUNDED TIME DOMAIN - An Alternative to NP-Complete Fragments of LTL
SN - 978-989-674-021-4
AU - Kamide N.
PY - 2010
SP - 536
EP - 539
DO - 10.5220/0002714805360539