Loading...
Send to Friend
 Bookmark
 Review List
  1. An equivalence based method for compositional verification of the linear temporal logic of constraint automata
An equivalence based method for compositional verification of the linear temporal logic of constraint automata
347 viewed

An equivalence based method for compositional verification of the linear temporal logic of constraint automata

Izadi, M

An equivalence based method for compositional verification of the linear temporal logic of constraint automata

Izadi, M ; Sharif University of Technology | 2006

347 Viewed
  1. Type of Document: Article
  2. DOI: 10.1016/j.entcs.2005.12.068
  3. Publisher: 2006
  4. Abstract:
  5. Constraint automaton is a formalism to capture the operational semantics of the channel based coordination language Reo. In general constraint automaton can be used as a formalism for modeling coordination of some components. In this paper we introduce a standard linear temporal logic and two fragments of it for expressing the properties of the systems modeled by constraint automata and show that the equivalence relation defined by Valmari et al. is the minimal compositional equivalence preserving that fragment of linear time temporal logic which has no next-time operator and has an extra operator distinguishing deadlocks and a slight modification of this equivalence is the minimal equivalence preserving linear time temporal logic without next-time operator. We present a compositional model checking method based on these equivalences for component-based systems modeled by labeled transition systems and constraint automata and a simplification of it for model checking the coordinating subsystems modeled by constraint automata. © 2006 Elsevier B.V. All rights reserved
  6. Keywords:
  7. Computer system recovery ; Constraint theory ; Equivalence classes ; Formal logic ; Mathematical models ; Optimization ; Component based systems ; Compositional verification ; Constraint automata ; Formal verification ; Automata theory
  8. Source: Electronic Notes in Theoretical Computer Science ; Volume 159, Issue 1 , 2006 , Pages 171-186 ; 15710661 (ISSN)
  9. URL: https://www.sciencedirect.com/science/article/pii/S1571066106002805