An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
Summary :
Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.
- Publication
- IEICE TRANSACTIONS on Information Vol.E93-D No.5 pp.994-1005
- Publication Date
- 2010/05/01
- Publicized
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.E93.D.994
- Type of Manuscript
- Special Section PAPER (Special Section on Formal Approach)
- Category
- Model Checking
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Takeshi NAGAOKA, Kozo OKANO, Shinji KUSUMOTO, "An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop" in IEICE TRANSACTIONS on Information,
vol. E93-D, no. 5, pp. 994-1005, May 2010, doi: 10.1587/transinf.E93.D.994.
Abstract: Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E93.D.994/_p
Copy
@ARTICLE{e93-d_5_994,
author={Takeshi NAGAOKA, Kozo OKANO, Shinji KUSUMOTO, },
journal={IEICE TRANSACTIONS on Information},
title={An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop},
year={2010},
volume={E93-D},
number={5},
pages={994-1005},
abstract={Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.},
keywords={},
doi={10.1587/transinf.E93.D.994},
ISSN={1745-1361},
month={May},}
Copy
TY - JOUR
TI - An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
T2 - IEICE TRANSACTIONS on Information
SP - 994
EP - 1005
AU - Takeshi NAGAOKA
AU - Kozo OKANO
AU - Shinji KUSUMOTO
PY - 2010
DO - 10.1587/transinf.E93.D.994
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E93-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2010
AB - Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.
ER -
English
