An on-the-fly tableau construction for a real-time temporal logic
| Autor: | Geilen, M.C.W., Dams, D.R., Joseph, M. |
|---|---|
| Přispěvatelé: | Electronic Systems, CompSOC Lab- Predictable & Composable Embedded Systems |
| Jazyk: | angličtina |
| Rok vydání: | 2000 |
| Předmět: |
Model checking
Theoretical computer science Computation tree logic TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Linear temporal logic Description logic Fragment (logic) Interval temporal logic Computer Science::Logic in Computer Science Temporal logic Temporal logic of actions Algorithm Mathematics |
| Zdroj: | Formal techniques in real-time and fault-tolerant systems : 6th international symposium, Pune, India, September 20-22, 2000 ; proceedings / FTRTFT 2000, 276-290 STARTPAGE=276;ENDPAGE=290;TITLE=Formal techniques in real-time and fault-tolerant systems : 6th international symposium, Pune, India, September 20-22, 2000 ; proceedings / FTRTFT 2000 Lecture Notes in Computer Science ISBN: 9783540410553 FTRTFT |
| ISSN: | 0302-9743 |
| DOI: | 10.1007/3-540-45352-0_23 |
| Popis: | Temporal logic is a useful tool for specifying correctness properties of reactive programs. In particular, real-time temporal logics have been developed for expressing quantitative timing aspects of systems. A tableau construction is an algorithm that translates a temporal logic formula into a finite-state automaton that accepts precisely all the models of the formula. It is a key ingredient to checking satisfiability of a formula as well as to the automata-theoretic approach to model checking. An improvement to the efficiency of tableau constructions has been the development of on-the-fly versions. In the real-time domain, tableau constructions have been developed for various logics and their complexities have been studied. However, there has been considerably less work aimed at improving and implementing them. In this paper, we present an on-the-fly tableau construction for a linear temporal logic with dense time, a fragment of Metric Interval Temporal Logic that is decidable in PSPACE. We have implemented a prototype of the algorithm and give experimental results. Being on-the-fly, our algorithm is expected to use less memory and to give smaller tableaux in many cases in practice than existing constructions. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|