Model-generation of a fictitious clock real-time logic using sharing trees

Jean François Raskin, Pierre Yves Schobbens, Laurent Ferier

Research output: Contribution to journalConference article

Abstract

We present first the logic MTL, a real-time temporal logic that is at the heart of the real-time specification language ALBERT. Since this logic is undecidable, we approximate it (using the theory of Abstract Interpretation) by its fictitious clock counterpart, MTLFC. We then present a symbolic tableau-based model generation decision procedure in EXPSPACE, which is theoretically optimal. In practice however, we see that the introduction of integer-valued prophecy variables will make it more efficient. From these variables, we reconstruct by reverting the process a logic that we call EXPSPACE, which can be decided in PSPACE, and has the same expressivity as MTLFC. Theory thus shows that memory space is the critical factor. However, the classical compaction of memory space by BDDs is not ideal here, since our integer variables would need to be encoded by booleans. Therefore, we use Sharing Trees instead, a compact data structure that can accommodate arbitrary data types. Preliminary results on this implementation are reported.

Original languageEnglish
Pages (from-to)113-131
Number of pages19
JournalElectronic Notes in Theoretical Computer Science
Volume23
Issue number2
DOIs
Publication statusPublished - 1 Dec 2001
EventSMC'99, First International Workshop on Symbolic Model Checking (Associated to FLoC'99, the 1999 Federated Logic Conference) - Trento, Italy
Duration: 6 Jul 19996 Jul 1999

Fingerprint

Clocks
Sharing
Logic
Real-time
Data storage equipment
Temporal logic
Specification languages
Data structures
Compaction
Abstract Interpretation
Integer
Tableau
Specification Languages
Decision Procedures
Temporal Logic
Data Structures
Model
Arbitrary
Heart

Cite this

@article{4055921cdc91468a9e0f8339e45b15d1,
title = "Model-generation of a fictitious clock real-time logic using sharing trees",
abstract = "We present first the logic MTL, a real-time temporal logic that is at the heart of the real-time specification language ALBERT. Since this logic is undecidable, we approximate it (using the theory of Abstract Interpretation) by its fictitious clock counterpart, MTLFC. We then present a symbolic tableau-based model generation decision procedure in EXPSPACE, which is theoretically optimal. In practice however, we see that the introduction of integer-valued prophecy variables will make it more efficient. From these variables, we reconstruct by reverting the process a logic that we call EXPSPACE, which can be decided in PSPACE, and has the same expressivity as MTLFC. Theory thus shows that memory space is the critical factor. However, the classical compaction of memory space by BDDs is not ideal here, since our integer variables would need to be encoded by booleans. Therefore, we use Sharing Trees instead, a compact data structure that can accommodate arbitrary data types. Preliminary results on this implementation are reported.",
author = "Raskin, {Jean Fran{\cc}ois} and Schobbens, {Pierre Yves} and Laurent Ferier",
year = "2001",
month = "12",
day = "1",
doi = "10.1016/S1571-0661(04)80672-8",
language = "English",
volume = "23",
pages = "113--131",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "2",

}

Model-generation of a fictitious clock real-time logic using sharing trees. / Raskin, Jean François; Schobbens, Pierre Yves; Ferier, Laurent.

In: Electronic Notes in Theoretical Computer Science, Vol. 23, No. 2, 01.12.2001, p. 113-131.

Research output: Contribution to journalConference article

TY - JOUR

T1 - Model-generation of a fictitious clock real-time logic using sharing trees

AU - Raskin, Jean François

AU - Schobbens, Pierre Yves

AU - Ferier, Laurent

PY - 2001/12/1

Y1 - 2001/12/1

N2 - We present first the logic MTL, a real-time temporal logic that is at the heart of the real-time specification language ALBERT. Since this logic is undecidable, we approximate it (using the theory of Abstract Interpretation) by its fictitious clock counterpart, MTLFC. We then present a symbolic tableau-based model generation decision procedure in EXPSPACE, which is theoretically optimal. In practice however, we see that the introduction of integer-valued prophecy variables will make it more efficient. From these variables, we reconstruct by reverting the process a logic that we call EXPSPACE, which can be decided in PSPACE, and has the same expressivity as MTLFC. Theory thus shows that memory space is the critical factor. However, the classical compaction of memory space by BDDs is not ideal here, since our integer variables would need to be encoded by booleans. Therefore, we use Sharing Trees instead, a compact data structure that can accommodate arbitrary data types. Preliminary results on this implementation are reported.

AB - We present first the logic MTL, a real-time temporal logic that is at the heart of the real-time specification language ALBERT. Since this logic is undecidable, we approximate it (using the theory of Abstract Interpretation) by its fictitious clock counterpart, MTLFC. We then present a symbolic tableau-based model generation decision procedure in EXPSPACE, which is theoretically optimal. In practice however, we see that the introduction of integer-valued prophecy variables will make it more efficient. From these variables, we reconstruct by reverting the process a logic that we call EXPSPACE, which can be decided in PSPACE, and has the same expressivity as MTLFC. Theory thus shows that memory space is the critical factor. However, the classical compaction of memory space by BDDs is not ideal here, since our integer variables would need to be encoded by booleans. Therefore, we use Sharing Trees instead, a compact data structure that can accommodate arbitrary data types. Preliminary results on this implementation are reported.

UR - http://www.scopus.com/inward/record.url?scp=18944371071&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)80672-8

DO - 10.1016/S1571-0661(04)80672-8

M3 - Conference article

AN - SCOPUS:18944371071

VL - 23

SP - 113

EP - 131

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 2

ER -