Analysis of Real-Time Systems with CTL Model Checkers | Zendy

Mustapha Bourahla | Zendy; Mohamed Benmohamed | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Analysis of Real-Time Systems with CTL Model Checkers

Author(s) -

Mustapha Bourahla,

Mohamed Benmohamed

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2004.08.057

Subject(s) - timed automaton , computation tree logic , automaton , model checking , computer science , property (philosophy) , state space , temporal logic , algorithm , theoretical computer science , mathematics , philosophy , statistics , epistemology

This paper presents a new method for model checking dense real-time systems. The dense real-time system is modeled by a timed automaton and the property is specified with the temporal logic TCTL. Specification of the TCTL property is reduced to CTL and its temporal constraints are captured in a new timed automaton. This timed automaton will be composed with the original timed automaton specifying the real-time system under analysis. Then, the product timed au- tomaton will be abstracted using partition refinement of state space based on strong bi-simulation. The result is an untimed automaton modulo the TCTL property which represents an equivalent finite state system to be model checked using existing CTL model checking tools

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research