Sciweavers

ICTAC
2007
Springer
13 years 10 months ago
On the Expressive Power of QLTL
LTL cannot express the whole class of ω-regular languages and several extensions have been proposed. Among them, Quantified propositional Linear Temporal Logic (QLTL), proposed b...
Zhilin Wu
IPPS
2007
IEEE
13 years 11 months ago
A Markov Reward Model for Software Reliability
A compositional method for estimating software reliability of many threaded programs is developed. The method uses estimates of the reliability of individual modules and the proba...
YoungMin Kwon, Gul Agha
QEST
2008
IEEE
13 years 11 months ago
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems
We present a new version of PROBDIVINE – a parallel tool for verification of probabilistic systems against properties formulated in linear temporal logic. Unlike the previous r...
Jiri Barnat, Lubos Brim, Ivana Cerná, Milan...
SACMAT
2009
ACM
13 years 11 months ago
Foundations for group-centric secure information sharing models
We develop the foundations for a theory of Group-Centric Secure Information Sharing (g-SIS), characterize a specific family of models in this arena and identify several direction...
Ram Krishnan, Ravi S. Sandhu, Jianwei Niu, William...
FSTTCS
2009
Springer
13 years 11 months ago
Automata and temporal logic over arbitrary linear time
Linear temporal logic was introduced in order to reason about reactive systems. It is often considered with respect to infinite words, to specify the behaviour of long-running sys...
Julien Cristau
CSL
2009
Springer
13 years 11 months ago
Craig Interpolation for Linear Temporal Languages
We study Craig interpolation for fragments and extensions of propositional linear temporal logic (PLTL). We consider various fragments of PLTL obtained by restricting the set of te...
Amélie Gheerbrant, Balder ten Cate
LATA
2009
Springer
13 years 11 months ago
Matching Trace Patterns with Regular Policies
Abstract. We consider policies that are described by regular expressions, finite automata, or formulae of linear temporal logic (LTL). Such policies are assumed to describe situat...
Franz Baader, Andreas Bauer 0002, Alwen Tiu
VMCAI
2010
Springer
13 years 11 months ago
Regular Linear Temporal Logic with Past
This paper upgrades Regular Linear Temporal Logic (RLTL) with past operators and complementation. RLTL is a temporal logic that extends the expressive power of linear temporal logi...
César Sánchez, Martin Leucker
ICSE
2004
IEEE-ACM
14 years 4 months ago
Efficient Decentralized Monitoring of Safety in Distributed Systems
We describe an efficient decentralized monitoring algorithm that monitors a distributed program's execution to check for violations of safety properties. The monitoring is ba...
Koushik Sen, Abhay Vardhan, Gul Agha, Grigore Rosu
CADE
2002
Springer
14 years 4 months ago
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains
Abstract. We investigate the combination of propositional SAT checkers with domain-specific theorem provers as a foundation for bounded model checking over infinite domains. Given ...
Harald Rueß, Leonardo Mendonça de Mou...