Author | Conference | Journal | Organization | Year | DOI
Look for results that meet for the following criteria:
Academic
Publications
SAT-based Abstraction Refinement for Real-time Systems

SAT-based Abstraction Refinement for Real-time Systems,10.1016/j.entcs.2006.09.034,Electronic Notes in Theoretical Computer Science,Stephanie Kemper,A

Edit
SAT-based Abstraction Refinement for Real-time Systems   (Citations: 8)
BibTex | RIS | RefWorks Download
In this paper, we present an abstraction refinement approach for model checking safety properties of real- time systems using SAT-solving. We present a faithful embedding of bounded model checking for systems of timed automata into propositional logic with linear arithmetic and prove correctness. With this logical representation, we achieve a linear-size representation of parallel composition and introduce a quick abstrac- tion technique that works uniformly for clocks, events, and states. When necessary, abstractions are refined by analysing spurious counterexamples using a promising extension of counterexample-guided abstraction refinement with syntactic information about Craig interpolants. To support generalisations, our overall approach identifies the algebraic and logical principles required for logic-based abstraction refinement.
Journal: Electronic Notes in Theoretical Computer Science - ENTCS , vol. 182, pp. 107-122, 2007
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
More »
    • ...[45], which uses bounded model checking and SAT-based techniques, [46], which is based on the region graph construction, and [47], for verifying PLC automata using UPPAAL [1]...

    Marta Z. Kwiatkowska, et al. A Framework for Verification of Software with Time and Probabilities

    • ...We conclude all behaviors in A are preserved in A � .F or a proof, we refer to [17]...

    Fei He, et al. Compositional Abstraction Refinement for Timed Systems

    • ...[8] which uses bounded model checking and SAT-based techniques, [22] which is based on the region graph construction, and [13] for verifying PLC automata using UPPAAL [19]...

    Marta Z. Kwiatkowska, et al. Stochastic Games for Verification of Probabilistic Timed Automata

    • ...In this paper, we build on the SAT-based approach for TA presented by Kemper and Platzer [14], but take into account the special transition characteristics of TCA...
    • ...We dene an abstraction function that is simple, yet powerful, and is able to preserve more information in the abstract case than the corresponding abstraction function in [14], which reduces the number of spurious counterexamples...
    • ...by zt xt. Note that linear arithmetic is equisatisable for rational and real variables [14]...
    • ...Using propositional formulas as intermediate representation (\front end"), we may fall back on the abstraction renement framework of [14] (\back end"), and, more importantly, we can take advantage of existing high-performance SAT-solving technologies...
    • ...In this section, we show how to adapt the abstraction technique of abstraction by merging omission (MO) [14] to our representation...
    • ...The major dierence between our abstraction function and the one presented in [14] is the fact that we do not in general map negative propositional variables to true (14a)...
    • ...The fully automatic heuristic presented in [14] (together with its optimisations) is a compromise between the drawbacks of the two alternatives: after rening a parameter (a), a xed number of traces (fractions of the unfolding depth turned out to be most promising) is ruled out (b) before rening the next symbol according to (a)...
    • ...Yet, in contrast to [14], our abstraction function does not remove negative propositional variables from the formula in case the map of merging is the identity for these...

    Stephanie Kemper. SAT-based Verification for Timed Component Connectors

    • ...A similar approach is also used in [28] for timed systems, and [29], [30] for hybrid systems...

    Alessandro Cimatti, et al. Structure-aware computation of predicate abstraction

Sort by:

Citations (8)

Share this on