Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
NFM
2011
306views Formal Methods» more  NFM 2011»
11 years 6 months ago
Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis
Synthesis of finite-state machines from linear-time temporal logic (LTL) formulas is an important formal specification debugging technique for reactive systems and can quickly ge...
Rüdiger Ehlers
AAI
2010
94views more  AAI 2010»
11 years 6 months ago
Sequence-Indexed Linear-Time Temporal Logic: Proof System and Application
In this paper, we propose a proof system for reasoning on certain specifications of secure authentication systems. For this purpose, a new logic, sequence-indexed linear-time temp...
Ken Kaneiwa, Norihiro Kamide
ENTCS
2002
143views more  ENTCS 2002»
11 years 11 months ago
Collecting Statistics over Runtime Executions
Abstract. We present an extension to linear-time temporal logic (LTL) that combines the temporal specification with the collection of statistical data. By collecting statistics ove...
Bernd Finkbeiner, Sriram Sankaranarayanan, Henny S...
ACTA
2004
97views more  ACTA 2004»
11 years 11 months ago
Past is for free: on the complexity of verifying linear temporal properties with past
We study the complexity of satisfiability and model-checking of the linear-time temporal logic with past (pltl). More precisely, we consider several fragments of pltl, depending o...
Nicolas Markey
IANDC
2007
132views more  IANDC 2007»
11 years 11 months ago
An automata-theoretic approach to constraint LTL
We consider an extension of linear-time temporal logic (LTL) with constraints interpreted over a concrete domain. We use a new automata-theoretic technique to show pspace decidabi...
Stéphane Demri, Deepak D'Souza
ENTCS
2006
114views more  ENTCS 2006»
11 years 11 months ago
Run-Time Checking of Dynamic Properties
We consider a first-order property specification language for run-time monitoring of dynamic systems. The language is based on a linear-time temporal logic and offers two kinds of...
Oleg Sokolsky, Usa Sammapun, Insup Lee, Jesung Kim
VLDB
1992
ACM
116views Database» more  VLDB 1992»
12 years 3 months ago
Supporting Lists in a Data Model (A Timely Approach)
This paper considers the problem of adding list as a type constructor to an object-oriented data model. In particular, we are concerned with how lists in a database can be constru...
Joel E. Richardson
LICS
2002
IEEE
12 years 4 months ago
Temporal Logic with Forgettable Past
We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL + Past (which in turn can be more succinct than LTL). We ...
François Laroussinie, Nicolas Markey, Ph. S...
FM
2003
Springer
174views Formal Methods» more  FM 2003»
12 years 5 months ago
Model-Checking TRIO Specifications in SPIN
We present a novel application on model checking through SPIN as a means for verifying purely descriptive specifications written in TRIO, a first order, linear-time temporal logic ...
Angelo Morzenti, Matteo Pradella, Pierluigi San Pi...
LFCS
2007
Springer
12 years 6 months ago
A Decidable Temporal Logic of Repeating Values
Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecida...
Stéphane Demri, Deepak D'Souza, Régi...
books