Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(6)
Automatic Verification
Linear Temporal Logic
Model Checking
Temporal Logic
Linear Time Temporal Logic
On The Fly
Related Publications
(73)
Improved Automata Generation for Linear Temporal Logic
Efficient Büchi Automata from LTL Formulae
Fast LTL to Büchi Automata Translation
MemoryEfficient Algorithms for the Verification of Temporal Properties
Optimizing Büchi Automata
Subscribe
Academic
Publications
Simple onthefly automatic verification of linear temporal logic
Simple onthefly automatic verification of linear temporal logic,Rob Gerth,Doron Peled,Moshe Y. Vardi,Pierre Wolper
Edit
Simple onthefly automatic verification of linear temporal logic
(
Citations: 418
)
BibTex

RIS

RefWorks
Download
Rob Gerth
,
Doron Peled
,
Moshe Y. Vardi
,
Pierre Wolper
We present a tableaubased algorithm for obtaining an automaton from a
temporal logic
formula. The algorithm is geared towards being used in
model checking
in an "onthefly" fas hion, that is the automaton can be constructed simultaneously with, and guided by, the generation of the model. In particular, it is possible to detect that a property does not hold by only const ructing part of the model and of the automaton. The algorithm can also be used to check the validity of a
temporal logic
assertion. Although the general problem is PSPACEcomplete, experiments show that our algorithm performs quite well on the temporal formulas typically encount ered in verification. While basing lineartime
temporal logic
modelchecking upon a transformation to automata is not new, the details of how to do this efficiently, and in "onthefly" f ashion have never been given.
Conference:
Protocol Specification, Testing and Verification  PSTV
, pp. 318, 1995
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.informatik.unitrier.de
)
Citation Context
(280)
...An online monitoring algorithm adapted from the onthefly verification of linear temporal logic [
10
] is also presented...
Guoquan Wu
,
et al.
Runtime Monitoring of Datacentric Temporal Properties for Web Service...
...Theorem 1: [
20
] A LTL formula f is satisfied iff there exists a path of states in the fautomata (finite with no successor at the last state or infinite)starting from the starting prestate and such that any occurrence of Future and Until modal operator in a state of the path fulfills its corresponding promise operand later (in the future) in the path...
...[
20
], [33]) use nested deepfirstsearch of fair loop or simple deep first search of fair SCC...
...The unwinding follows the Algorithm 3. Those unwound formulas are valid formulas and of the form pres( ) ) disjpres( ) where disjpres( ) is the classical unwinding of formulas at the state of tableau [
20
], [33]...
Francois Hantry
,
et al.
Detection of Conflicting Compliance Rules
...The fact that logics such as LTL (lineartime temporal logic) or CTL (computation tree logic) can be efficiently translated into corresponding automata [
10
, 11, 26, 28 ]h as facilitated their integration into main verification tools...
Kevin D. Jones
,
et al.
Analog property checkers: a DDR2 case study
...Efficient translation implementations have been developed in [
15
], [16]...
Stephen L. Smith
,
et al.
Optimal Path Planning under Temporal Logic Constraints
...LTL translation algorithm was described in [
26
]...
...Does size matter? The focus of almost all LTL translation papers, starting with [
26
], has been on minimizing automata size...
Kristin Y. Rozier
,
et al.
LTL satisfiability checking
References
(19)
The tableau method for temporal logic: an overview
(
Citations: 139
)
P. Wolper
Published in 1985.
The complexity of propositional linear temporal logics
(
Citations: 472
)
A. Prasad Sistla
,
Edmund M. Clarke
Journal:
Journal of The ACM  JACM
, vol. 32, no. 3, pp. 733749, 1985
Checking that finite state concurrent programs satisfy their linear specification
(
Citations: 470
)
Orna Lichtenstein
,
Amir Pnueli
Conference:
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  POPL
, pp. 97107, 1985
Temporal Logic Can Be More Expressive
(
Citations: 444
)
Pierre Wolper
Conference:
IEEE Symposium on Foundations of Computer Science  FOCS
, pp. 340348, 1981
A Decision Algorithm for Full Propositional Temporal Logic
(
Citations: 64
)
Yonit Kesten
,
Zohar Manna
,
Hugh Mcguire
,
Amir Pnueli
Conference:
Computer Aided Verification  CAV
, pp. 97109, 1993
Sort by:
Citations
(418)
Runtime Monitoring of Datacentric Temporal Properties for Web Services
Guoquan Wu
,
Jun Wei
,
Chunyang Ye
,
Xiaozhe Shao
,
Hua Zhong
,
Tao Huang
Conference:
International Conference on Web Services  ICWS
, 2011
Verifying Web Services Composition based on LTL and colored Petri Net
Jihan Zhu
,
Kan Zhang
,
Guangquan Zhang
Conference:
International Conference on Computer Science & Education  ICCSE
, 2011
Detection of Conflicting Compliance Rules
Francois Hantry
,
MohandSaid Hacid
,
Romuald Thion
Conference:
Enterprise Distributed Object Computing Conference  EDOS
, 2011
Declarative specification and verification of service choreographies
(
Citations: 14
)
Marco Montali
,
Maja Pesic
,
Wil M. P. van der Aalst
,
Federico Chesani
,
Paola Mello
,
Sergio Storari
Journal:
ACM Transactions on The Web  TWEB
, vol. 4, no. 1, pp. 162, 2010
Analog property checkers: a DDR2 case study
(
Citations: 3
)
Kevin D. Jones
,
Victor Konrad
,
Dejan Nickovic
Journal:
Formal Methods in System Design  FMSD
, vol. 36, no. 2, pp. 114130, 2010