publication . Book . Part of book or chapter of book . 2003

Bounded Model Checking for Past LTL

Benedetti, M.; Alessandro Cimatti;
  • Published: 01 Jan 2003
The introduction of Past Operators enables to produce more natural formulation of a wide class of properties of reactive systems, compared to traditional pure future temporal logics. For this reason, past temporal logics are gaining increasing interest in several application areas, ranging from Requirement Engineering to Formal Verification and Model Checking. We show how SAT-based Bounded Model Checking techniques can be extended to deal with Linear Temporal Logics with Past Operators (PLTL). Though apparently simple, this task turns out to be absolutely non-trivial when tackled in its full generality. We discuss a bounded semantics for PLTL, we show that it is...
free text keywords: Theoretical computer science, Encoding (memory), Bounded function, Discrete mathematics, Computation tree logic, Reactive system, Formal verification, Operator (computer programming), Computer science, Model checking, Semantics
Download fromView all 2 versions
Part of book or chapter of book
Provider: UnpayWall
Part of book or chapter of book
Provider: Crossref
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue