Paper Info
Title
An Automata-based Approach for CTL*; With Constraints
Abstract
We introduce a general definition for a family of branching-time logics that extend CTL* by allowing constraints between variables at the atomic level. These constraints allow to compare values of variables at different states of the model. We define an automata-theoretic approach to solve verification problems for such extensions. Our method is based on a finite abstraction of the infinite state space and a symbolic representation of the models that generalizes several approaches used for extensions of the linear-time logic LTL with constraints. We extend and combine several constructions involving alternating tree automata. We apply this approach to prove decidability and optimal complexity results for particular instances of CTL* extensions whenever an abstraction of the models verifying a ''nice'' property can be computed. These theoretical results generalize several results on LTL with constraints where such nice abstractions are used.
Year
DOI
Venue
2009
10.1016/j.entcs.2009.05.040
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
atomic level,different state,infinite state space,nice abstraction,Automata approach,Model-checking,Temporal-logic,general definition,finite abstraction,Automata-based Approach,optimal complexity result,linear-time logic LTL,automata-theoretic approach,branching-time logic
Discrete mathematics,Algebra,Automaton,CTL*,Mathematics
Journal
Volume
ISSN
Citations 
239,
Electronic Notes in Theoretical Computer Science
2
PageRank 
References 
Authors
0.40
12
1
Name
Order
Citations
PageRank
Régis Gascon1765.23