Quantifier-free encoding of invariants for hybrid systems

被引：0
|
作者：
Alessandro Cimatti
Sergio Mover
Stefano Tonetta
机构：
[1] Fondazione Bruno Kessler,
来源：
Formal Methods in System Design | 2014年 / 45卷
关键词：
Satisfiability modulo theory; Hybrid systems; Bounded model checking;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
Hybrid systems are a clean modeling framework for embedded systems, which feature integrated discrete and continuous dynamics. A well-known source of complexity comes from the time invariants, which represent an implicit quantification of a constraint over all time points of a continuous transition.
引用
收藏
页码：165 / 188
页数：23
相关论文
共 50 条
  • [21] Simplification of quantifier-free formulae over ordered fields
    Dolzmann, A
    Sturm, T
    JOURNAL OF SYMBOLIC COMPUTATION, 1997, 24 (02) : 209 - 231
  • [22] An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
    Angelo Brillout
    Daniel Kroening
    Philipp Rümmer
    Thomas Wahl
    Journal of Automated Reasoning, 2011, 47 : 341 - 367
  • [23] Deciding Quantifier-free Definability in Finite Algebraic Structures
    Campercholi, Miguel
    Tellechea, Mauricio
    Ventura, Pablo
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2020, 348 : 23 - 41
  • [24] Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
    Brillout, Angelo
    Kroening, Daniel
    Ruemmer, Philipp
    Wahl, Thomas
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2011, 6538 : 88 - +
  • [25] An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
    Brillout, Angelo
    Kroening, Daniel
    Ruemmer, Philipp
    Wahl, Thomas
    JOURNAL OF AUTOMATED REASONING, 2011, 47 (04) : 341 - 367
  • [26] Compositional truth with propositional tautologies and quantifier-free correctness
    Wcislo, Bartosz
    ARCHIVE FOR MATHEMATICAL LOGIC, 2024, 63 (1-2) : 239 - 257
  • [27] Quantifier-Free Interpolation in Combinations of Equality Interpolating Theories
    Bruttomesso, Roberto
    Ghilardi, Silvio
    Ranise, Silvio
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2014, 15 (01)
  • [28] WITTGENSTEIN'S ELIMINATION OF IDENTITY FOR QUANTIFIER-FREE LOGIC
    LAMPERT, T. I. M. M.
    Saebel, Markus
    REVIEW OF SYMBOLIC LOGIC, 2021, 14 (01): : 1 - 21
  • [29] Quantifier-free axioms for constructive affine plane geometry
    Suppes, P
    SYNTHESE, 2000, 125 (1-2) : 263 - 281
  • [30] A tableau calculus for quantifier-free set theoretic formulae
    Beckert, B
    Hartmer, U
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1998, 1397 : 93 - 107
12345