On Verification of Linear Occurrence Properties of Real-Time Systems | Zendy

Changil Choe | Zendy; Dang Van Hung | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

On Verification of Linear Occurrence Properties of Real-Time Systems

Author(s) -

Changil Choe,

Dang Van Hung

Publication year - 2008

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.2008.03.088

Subject(s) - dependability , computer science , probabilistic logic , automaton , monotonic function , class (philosophy) , probabilistic automaton , extension (predicate logic) , theoretical computer science , algorithm , computation , integer (computer science) , mathematics , programming language , artificial intelligence , mathematical analysis , software engineering

Duration Calculus of Weakly Monotonic Time (WDC) is an extension of DC to allow description of discrete processes where several steps of computation can occur at the same time point. In this paper, we introduce Linear Occurrence Invariants (LOI) using WDC and give an algorithm to check real-time automata for LOI by solving integer programming problems. LOI can be used effectively to specify system requirements in some cases including when the system is considered under the true synchrony assumption. We also extend WDC probabilistically to express dependability requirements of real-time systems and develop a technique to check deterministic probabilistic real-time automata for a class of probabilistic WDC formulas

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