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

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

Résultats de recherche: Contribution à un journal/une revue???researchoutput.researchoutputtypes.contributiontojournal.conferencearticle???Revue par des pairs


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.

langue originaleAnglais
Pages (de - à)113-131
Nombre de pages19
journalElectronic Notes in Theoretical Computer Science
Numéro de publication2
Les DOIs
Etat de la publicationPublié - 1 déc. 2001
EvénementSMC'99, First International Workshop on Symbolic Model Checking (Associated to FLoC'99, the 1999 Federated Logic Conference) - Trento, Italie
Durée: 6 juil. 19996 juil. 1999

Empreinte digitale Examiner les sujets de recherche de « Model-generation of a fictitious clock real-time logic using sharing trees ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation