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
(3)
Linear Temporal Logic
Model Checking
Lower Bound
Subscribe
Academic
Publications
Minimal Büchi Automata for Certain Classes of LTL Formulas
Minimal Büchi Automata for Certain Classes of LTL Formulas,10.1109/DepCoS-RELCOMEX.2009.31,J. Cichon,Adam Czubak,A. Jasinski
Edit
Minimal Büchi Automata for Certain Classes of LTL Formulas
(
Citations: 1
)
BibTex
|
RIS
|
RefWorks
Download
J. Cichon
,
Adam Czubak
,
A. Jasinski
In this paper we calculate the minimal number of states of Buchi automata which encode some classes of
linear temporal logic
(LTL) formulas that are frequently used in model checking. Among others, we show that the minimal size of a Buchi automaton accepting the formula Pi0p1 Lambda ... Lambda Pi0pn is n+1, the minimal size of Buchi automaton accepting the formula 0p1Lambda ... Lambda0pn is 2n and the minimal size of a Buchi automaton accepting the formula 0(p1Lambda0p1)Lambda...Lambda(pnLambda0pn) is 3n. Our results may be used for verification of the quality of algorithms which automatically translate LTL formulas into Buchi automata and for improving the quality and speed of such translators. In the last section of this paper we compare our
lower bound
estimations to Buchi automata generated by two currently used translators: LTL2BA and SPOT. We have checked, among others, that the LTL2BA translator generates a Buchi automaton with 25 states and the SPOT translator generates an automaton with 31 states for the formula 0(p1Lambda0(p2Lambda0p3))Lambda0(q1Lambda0(q2Lambda0q3)), while the minimal required number of states is 16.
Conference:
International Conference on Dependability of Computer Systems - DEPCOS
, 2009
DOI:
10.1109/DepCoS-RELCOMEX.2009.31
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.
(
ieeexplore.ieee.org
)
(
ieeexplore.ieee.org
)
Citation Context
(1)
...Since the value of novel encoding techniques lies in increased scalability ,w e evaluate our novel encodings in the context of LTL satisfiability checking, utilizing a comprehensive and challenging collection of widely-used benchmark formulas [
7
, 14, 23, 35]...
...Input Formulas. We employed a widely-used [
7
, 14, 23, 35] collection of benchmark formulas, established by [35]...
Kristin Y. Rozier
,
et al.
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking
References
(9)
The spin model checker
(
Citations: 502
)
G. Holzmann
Journal:
IEEE Transactions on Software Engineering - TSE
, 1997
Simple on-the-fly automatic verification of linear temporal logic
(
Citations: 418
)
Rob Gerth
,
Doron Peled
,
Moshe Y. Vardi
,
Pierre Wolper
Conference:
Protocol Specification, Testing and Verification - PSTV
, pp. 3-18, 1995
Fast LTL to Büchi Automata Translation
(
Citations: 199
)
Paul Gastin
,
Denis Oddoux
Conference:
Computer Aided Verification - CAV
, pp. 53-65, 2001
Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient
(
Citations: 22
)
Jaco Geldenhuys
,
Antti Valmari
Conference:
Tools and Algorithms for Construction and Analysis of Systems - TACAS
, pp. 205-219, 2004
LTL Satisfiability Checking
(
Citations: 24
)
Kristin Y. Rozier
,
Moshe Y. Vardi
Conference:
International Workshop on Model Checking of Software - SPIN
, pp. 149-167, 2007
Sort by:
Citations
(1)
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking
Kristin Y. Rozier
,
Moshe Y. Vardi