A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances Method
In generating invariants for hybrid systems, a main source of intractability is that transition relations are first-order assertions over current-state variables and next-state variables, which doubles the number of system variables and introduces many more free variables. The more variables, the le...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
MDPI AG
2020-05-01
|
Series: | Information |
Subjects: | |
Online Access: | https://www.mdpi.com/2078-2489/11/5/246 |
id |
doaj-d5775f4b56064c33bc409c0c846c20b2 |
---|---|
record_format |
Article |
spelling |
doaj-d5775f4b56064c33bc409c0c846c20b22020-11-25T02:40:06ZengMDPI AGInformation2078-24892020-05-011124624610.3390/info11050246A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances MethodHonghui He0Jinzhao Wu1Chengdu Institute of Computer Application, Chinese Academy of Sciences, Chengdu 610041, ChinaChengdu Institute of Computer Application, Chinese Academy of Sciences, Chengdu 610041, ChinaIn generating invariants for hybrid systems, a main source of intractability is that transition relations are first-order assertions over current-state variables and next-state variables, which doubles the number of system variables and introduces many more free variables. The more variables, the less tractability and, hence, solving the algebraic constraints on complete inductive conditions by a comprehensive Gröbner basis is very expensive. To address this issue, this paper presents a new, complete method, called the Citing Instances Method (CIM), which can eliminate the free variables and directly solve for the complete inductive conditions. An instance means the verification of a proposition after instantiating free variables to numbers. A lattice array is a key notion in this paper, which is essentially a finite set of instances. Verifying that a proposition holds over a Lattice Array suffices to prove that the proposition holds in general; this interesting feature inspires us to present CIM. On one hand, instead of computing a comprehensive Gröbner basis, CIM uses a Lattice Array to generate the constraints in parallel. On the other hand, we can make a clever use of the parallelism of CIM to start with some constraint equations which can be solved easily, in order to determine some parameters in an early state. These solved parameters benefit the solution of the rest of the constraint equations; this process is similar to the domino effect. Therefore, the constraint-solving tractability of the proposed method is strong. We show that some existing approaches are only special cases of our method. Moreover, it turns out CIM is more efficient than existing approaches under parallel circumstances. Some examples are presented to illustrate the practicality of our method.https://www.mdpi.com/2078-2489/11/5/246citing instances methodcomprehensive Gröbner basishybrid systemlattice arrayinvariant |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Honghui He Jinzhao Wu |
spellingShingle |
Honghui He Jinzhao Wu A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances Method Information citing instances method comprehensive Gröbner basis hybrid system lattice array invariant |
author_facet |
Honghui He Jinzhao Wu |
author_sort |
Honghui He |
title |
A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances Method |
title_short |
A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances Method |
title_full |
A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances Method |
title_fullStr |
A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances Method |
title_full_unstemmed |
A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances Method |
title_sort |
new approach to nonlinear invariants for hybrid systems based on the citing instances method |
publisher |
MDPI AG |
series |
Information |
issn |
2078-2489 |
publishDate |
2020-05-01 |
description |
In generating invariants for hybrid systems, a main source of intractability is that transition relations are first-order assertions over current-state variables and next-state variables, which doubles the number of system variables and introduces many more free variables. The more variables, the less tractability and, hence, solving the algebraic constraints on complete inductive conditions by a comprehensive Gröbner basis is very expensive. To address this issue, this paper presents a new, complete method, called the Citing Instances Method (CIM), which can eliminate the free variables and directly solve for the complete inductive conditions. An instance means the verification of a proposition after instantiating free variables to numbers. A lattice array is a key notion in this paper, which is essentially a finite set of instances. Verifying that a proposition holds over a Lattice Array suffices to prove that the proposition holds in general; this interesting feature inspires us to present CIM. On one hand, instead of computing a comprehensive Gröbner basis, CIM uses a Lattice Array to generate the constraints in parallel. On the other hand, we can make a clever use of the parallelism of CIM to start with some constraint equations which can be solved easily, in order to determine some parameters in an early state. These solved parameters benefit the solution of the rest of the constraint equations; this process is similar to the domino effect. Therefore, the constraint-solving tractability of the proposed method is strong. We show that some existing approaches are only special cases of our method. Moreover, it turns out CIM is more efficient than existing approaches under parallel circumstances. Some examples are presented to illustrate the practicality of our method. |
topic |
citing instances method comprehensive Gröbner basis hybrid system lattice array invariant |
url |
https://www.mdpi.com/2078-2489/11/5/246 |
work_keys_str_mv |
AT honghuihe anewapproachtononlinearinvariantsforhybridsystemsbasedonthecitinginstancesmethod AT jinzhaowu anewapproachtononlinearinvariantsforhybridsystemsbasedonthecitinginstancesmethod AT honghuihe newapproachtononlinearinvariantsforhybridsystemsbasedonthecitinginstancesmethod AT jinzhaowu newapproachtononlinearinvariantsforhybridsystemsbasedonthecitinginstancesmethod |
_version_ |
1724783044989026304 |