scholarly journals SMT Encoding of Hybrid Systems in dReal

10.29007/s3b9 ◽  
2018 ◽  
Author(s):  
Kyungmin Bae ◽  
Soonho Kong ◽  
Sicun Gao
Keyword(s):  
Model Checking ◽  
Differential Equations ◽  
Ordinary Differential Equations ◽  
Hybrid Systems ◽  
Bounded Model Checking ◽  
Satisfiability Modulo Theories ◽  
Real Numbers ◽  
The Real ◽  
Real Functions ◽  
Nonlinear Hybrid

Analysis problems of hybrid systems, involving nonlinear real functions and ordinary differential equations, can be reduced to SMT (satisfiability modulo theories) problems over the real numbers. The dReal solver can automatically check the satisfiability of such SMT formulas up to a given precision δ > 0. This paper explains how bounded model checking problems of hybrid systems are encoded in dReal. In particular, a novel SMT syntax of dReal enables to effectively represent networks of hybrid systems in a modular way. We illustrate SMT encoding in dReal with simple nonlinear hybrid systems.

scholarly journals Representing hybrid automata by action language modulo theories

2017 ◽  
Vol 17 (5-6) ◽  
pp. 924-941 ◽  
Author(s):  
JOOHYUNG LEE ◽  
NIKHIL LONEY ◽  
YUNSONG MENG
Keyword(s):  
Differential Equations ◽  
Ordinary Differential Equations ◽  
Satisfiability Modulo Theories ◽  
Prototype System ◽  
Hybrid Automata ◽  
Action Languages ◽  
Smt Solver ◽  
Action Language ◽  
Linear Hybrid Automata ◽  
Answer Set

AbstractBoth hybrid automata and action languages are formalisms for describing the evolution of dynamic systems. This paper establishes a formal relationship between them. We show how to succinctly represent hybrid automata in an action language which in turn is defined as a high-level notation for answer set programming modulo theories—an extension of answer set programs to the first-order level similar to the way satisfiability modulo theories (SMT) extends propositional satisfiability (SAT). We first show how to represent linear hybrid automata with convex invariants by an action language modulo theories. A further translation into SMT allows for computing them using SMT solvers that support arithmetic over reals. Next, we extend the representation to the general class of non-linear hybrid automata allowing even non-convex invariants. We represent them by an action language modulo ordinary differential equations, which can be compiled into satisfiability modulo ordinary differential equations. We present a prototype systemcplus2aspmtbased on these translations, which allows for a succinct representation of hybrid transition systems that can be computed effectively by the state-of-the-art SMT solverdReal.

scholarly journals Solution of Linear Fuzzy Fractional Differential Equations Using Fuzzy Natural Transform

2021 ◽  
pp. 41-65
Author(s):  
Hameeda Oda Al-Humedi ◽  
Shaimaa Abdul-Hussein Kadhim
Keyword(s):  
Differential Equations ◽  
Ordinary Differential Equations ◽  
Fractional Differential Equations ◽  
Wide Range ◽  
Real Functions ◽  
Fractional Models ◽  
Fractional Differential ◽  
Fuzzy Fractional Differential Equations

The purpose of this paper is to apply the fuzzy natural transform (FNT) for solving linear fuzzy fractional ordinary differential equations (FFODEs) involving fuzzy Caputo’s H-difference with Mittag-Leffler laws. It is followed by proposing new results on the property of FNT for fuzzy Caputo’s H-difference. An algorithm was then applied to find the solutions of linear FFODEs as fuzzy real functions. More specifically, we first obtained four forms of solutions when the FFODEs is of order α∈(0,1], then eight systems of solutions when the FFODEs is of order α∈(1,2] and finally, all of these solutions are plotted using MATLAB. In fact, the proposed approach is an effective and practical to solve a wide range of fractional models.

scholarly journals ARCH-COMP17 Category Report: Bounded Model Checking of Hybrid Systems with Piecewise Constant Dynamics

10.29007/rvk6 ◽  
2018 ◽  
Author(s):  
Lei Bu ◽  
Rajarshi Ray ◽  
Stefan Schupp
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Hybrid Systems ◽  
Bounded Model Checking ◽  
Benchmark Problems ◽  
Future Event ◽  
Alphabetical Order ◽  
Piecewise Constant ◽  
The Future ◽  
Friendly Competition

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, three tools have been applied to solve three different benchmark problems in the category ofbounded model checking of hybrid systems with piecewise constant dynamics (in alphabetical order): BACH, HyDRA, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools and we also welcome more tools to join in this friendly competition in the future event.

scholarly journals ARCH-COMP19 Category Report: Bounded Model Checking of Hybrid Systems with Piecewise Constant Dynamics

10.29007/g965 ◽  
2019 ◽  
Author(s):  
Lei Bu ◽  
Rajarshi Ray ◽  
Stefan Schupp
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Hybrid Systems ◽  
Bounded Model Checking ◽  
Optimization Techniques ◽  
Benchmark Problems ◽  
Future Event ◽  
Alphabetical Order ◽  
Piecewise Constant ◽  
Friendly Competition

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In its third edition, three tools have been applied to solve three different benchmark problems in the category ofbounded model checking of hybrid systems with piecewise constant dynamics (in alphabetical order): BACH, HyDRA, and XSpeed. Compare to last year, HyDRA is equipped with new optimization techniques and the performance is improved accordingly. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools and we also welcome more tools to join in this friendly competition in the future event.

scholarly journals ARCH-COMP18 Category Report: Bounded Model Checking of Hybrid Systems with Piecewise Constant Dynamics

10.29007/q5tq ◽  
2018 ◽  
Author(s):  
Lei Bu ◽  
Rajarshi Ray ◽  
Stefan Schupp
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Hybrid Systems ◽  
Bounded Model Checking ◽  
Benchmark Problems ◽  
Future Event ◽  
Alphabetical Order ◽  
Piecewise Constant ◽  
The Future ◽  
Friendly Competition

This report presents results of a friendly competition for formal verification of contin- uous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In its second edition, three tools have been applied to solve three differ- ent benchmark problems in the category ofbounded model checking of hybrid systems with piecewise constant dynamics (in alphabetical order): BACH, HyDRA, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools and we also welcome more tools to join in this friendly competition in the future event.

On α-Polynomial Regular Functions, with Applications to Ordinary Differential Equations

2014 ◽  
Vol 57 (2) ◽  
pp. 405-421 ◽  
Author(s):  
Peter Fenton ◽  
Janne Grohn ◽  
Janne Heittokangas ◽  
John Rossi ◽  
Jouni Rattya
Keyword(s):  
Differential Equations ◽  
Ordinary Differential Equations ◽  
Unit Disc ◽  
Maximum Modulus ◽  
Linear Differential Equations ◽  
Real Numbers ◽  
Regular Functions ◽  
Function Classes ◽  
Finite Set ◽  
Linear Differential

AbstractThis research deals with properties of polynomial regular functions, which were introduced in a recent study concerning Wiman-Valiron theory in the unit disc. The relation of polynomial regular functions to a number of function classes is investigated. Of particular interest is the connection to the growth class Gα, which is closely associated with the theory of linear differential equations with analytic coefficients in the unit disc. If the coefficients are polynomial regular functions, then it turns out that a finite set of real numbers containing all possible maximum modulus orders of solutions can be found. This is in contrast to what is known about the case when the coefficients belong to Gα.

Sign in / Sign up

Export Citation Format

Share Document