Showing 1–33 of 33 results for author: Zhan, N

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes

Authors: Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan

Abstract: We present a tool called HHLPar for verifying hybrid systems modelled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is built upon a Hybrid Hoare Logic for HCSP, which is able to reason about continuous-time properties of differential equations, as well as communication and parallel composition of parallel HCSP processes with the help of parameterised trace assertions and their synchr… ▽ More We present a tool called HHLPar for verifying hybrid systems modelled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is built upon a Hybrid Hoare Logic for HCSP, which is able to reason about continuous-time properties of differential equations, as well as communication and parallel composition of parallel HCSP processes with the help of parameterised trace assertions and their synchronization. The logic was formalised and proved to be sound in Isabelle/HOL, which constitutes a trustworthy foundation for the verification conducted by HHLPar. HHLPar implements the Hybrid Hoare Logic in Python and supports automated verification: On one hand, it provides functions for symbolically decomposing HCSP processes, generating specifications for separate sequential processes and then composing them via synchronization to obtain the final specification for the whole parallel HCSP processes; On the other hand, it is integrated with external solvers for handling differential equations and real arithmetic properties. We have conducted experiments on a simplified cruise control system to validate the performance of the tool. △ Less

Submitted 11 July, 2024; originally announced July 2024.

Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets

Authors: Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan

Abstract: Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local reasoning capabilities. Synthesizing Craig interpolants is the cornerstone of these techniques. In this paper, we investigate nonlinear Craig interpolant synthesis for two polynomial formulas of the general form, essenti… ▽ More Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local reasoning capabilities. Synthesizing Craig interpolants is the cornerstone of these techniques. In this paper, we investigate nonlinear Craig interpolant synthesis for two polynomial formulas of the general form, essentially corresponding to the underlying mathematical problem to separate two disjoint semialgebraic sets. By combining the homogenization approach with existing techniques, we prove the existence of a novel class of non-polynomial interpolants called semialgebraic interpolants. These semialgebraic interpolants subsume polynomial interpolants as a special case. To the best of our knowledge, this is the first existence result of this kind. Furthermore, we provide complete sum-of-squares characterizations for both polynomial and semialgebraic interpolants, which can be efficiently solved as semidefinite programs. Examples are provided to demonstrate the effectiveness and efficiency of our approach. △ Less

Submitted 30 June, 2024; originally announced July 2024.

Comments: 21 pages (with appendix); accepted by the 26th International Symposium on Formal Methods (FM2024)

Switching Controller Synthesis for Hybrid Systems Against STL Formulas

Authors: Han Su, Shenghua Feng, Sinong Zhan, Naijun Zhan

Abstract: Switching controllers play a pivotal role in directing hybrid systems (HSs) towards the desired objective, embodying a ``correct-by-construction'' approach to HS design. Identifying these objectives is thus crucial for the synthesis of effective switching controllers. While most of existing works focus on safety and liveness, few of them consider timing constraints. In this paper, we delves into t… ▽ More Switching controllers play a pivotal role in directing hybrid systems (HSs) towards the desired objective, embodying a ``correct-by-construction'' approach to HS design. Identifying these objectives is thus crucial for the synthesis of effective switching controllers. While most of existing works focus on safety and liveness, few of them consider timing constraints. In this paper, we delves into the synthesis of switching controllers for HSs that meet system objectives given by a fragment of STL, which essentially corresponds to a reach-avoid problem with timing constraints. Our approach involves iteratively computing the state sets that can be driven to satisfy the reach-avoid specification with timing constraints. This technique supports to create switching controllers for both constant and non-constant HSs. We validate our method's soundness, and confirm its relative completeness for a certain subclass of HSs. Experiment results affirms the efficacy of our approach. △ Less

Submitted 24 June, 2024; originally announced June 2024.

Piecewise Linear Expectation Analysis via $k$-Induction for Probabilistic Programs

Authors: Tengshun Yang, Hongfei Fu, Jingyu Ke, Naijun Zhan, Shiyang Wu

Abstract: Quantitative analysis of probabilistic programs aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability, and plays a crucial role in the verification of probabilistic programs. Along this line of research, most existing works consider numerical bounds over the whole state space monolithically and do not consider piecewise bounds. Clearly,… ▽ More Quantitative analysis of probabilistic programs aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability, and plays a crucial role in the verification of probabilistic programs. Along this line of research, most existing works consider numerical bounds over the whole state space monolithically and do not consider piecewise bounds. Clearly, monolithic bounds are either conservative, or not expressive and succinct enough in general. To derive more succinct, expressive and precise numerical bounds for probabilistic properties, we propose a novel approach for synthesizing piecewise linear bounds in this work. To this end, we first show how to extract a piecewise feature w.r.t. a given quantitative property from a probabilistic program using latticed $k$-induction that captures a wide and representative class of piecewise bound functions. Second, we develop an algorithmic approach to synthesize piecewise linear upper and lower bounds from the piecewise feature, for which we show that the synthesis of piecewise linear bounds can be reduced to bilinear programming. Third, we implement our approach with the bilinear programming solver Gurobi. The experimental results indicate that our approach is capable of generating tight or even accurate piecewise linear bounds for an extensive set of benchmarks compared with the state of the art. △ Less

Submitted 26 March, 2024; originally announced March 2024.

Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems

Authors: Bohua Zhan, Xiong Xu, Qiang Gao, Zekun Ji, Xiangyu Jin, Shuling Wang, Naijun Zhan

Abstract: We introduce Mars 2.0 for modeling, analysis, verification and code generation of Cyber-Physical Systems. Mars 2.0 integrates Mars 1.0 with several important extensions and improvements, allowing the design of cyber-physical systems using the combination of AADL and Simulink/Stateflow, which provide a unified graphical framework for modeling the functionality, physicality and architecture of the s… ▽ More We introduce Mars 2.0 for modeling, analysis, verification and code generation of Cyber-Physical Systems. Mars 2.0 integrates Mars 1.0 with several important extensions and improvements, allowing the design of cyber-physical systems using the combination of AADL and Simulink/Stateflow, which provide a unified graphical framework for modeling the functionality, physicality and architecture of the system to be developed. For a safety-critical system, formal analysis and verification of its combined AADL and Simulink/Stateflow model can be conducted via the following steps. First, the toolchain automatically translates AADL and Simulink/Stateflow models into Hybrid CSP (HCSP), an extension of CSP for formally modeling hybrid systems. Second, the HCSP processes can be simulated using the HCSP simulator, and to complement incomplete simulation, they can be verified using the Hybrid Hoare Logic prover in Isabelle/HOL, as well as the more automated HHLPy prover. Finally, implementations in SystemC or C can be automatically generated from the verified HCSP processes. The transformation from AADL and Simulink/Stateflow to HCSP, and the one from HCSP to SystemC or C, are both guaranteed to be correct with formal proofs. This approach allows model-driven design of safety-critical cyber-physical systems based on graphical and formal models and proven-correct translation procedures. We demonstrate the use of the toolchain on several benchmarks of varying complexity, including several industrial-sized examples. △ Less

Submitted 5 March, 2024; originally announced March 2024.

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes

Authors: Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, Naijun Zhan

Abstract: Hybrid Communicating Sequential Processes (HCSP) is a formal model for hybrid systems, including primitives for evolution along an ordinary differential equation (ODE), communication, and parallel composition. Code generation is needed to convert HCSP models into code that can be executed in practice, and the correctness of this conversion is essential to ensure that the generated code accurately… ▽ More Hybrid Communicating Sequential Processes (HCSP) is a formal model for hybrid systems, including primitives for evolution along an ordinary differential equation (ODE), communication, and parallel composition. Code generation is needed to convert HCSP models into code that can be executed in practice, and the correctness of this conversion is essential to ensure that the generated code accurately reflects the formal model. In this paper, we propose a code generation algorithm from HCSP to C with POSIX library for concurrency. The main difficulties include how to bridge the gap between the synchronized communication model in HCSP and the use of mutexes for synchronization in C, and how to discretize evolution along ODEs and support interrupt of ODE evolution by communication. To prove the correctness of code generation, we define a formal semantics for POSIX C, and build transition system models for both HCSP and C programs. We then define an approximate bisimulation relation between traces of transition systems, and show that under certain robustness conditions for HCSP, the generated C program is approximately bisimilar to the original model. Finally, we evaluate the code generation algorithm on a detailed model for automatic cruise control, showing its utility on real-world examples. △ Less

Submitted 26 February, 2024; v1 submitted 23 February, 2024; originally announced February 2024.

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming

Authors: Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi, Zhihong Yang

Abstract: Constraint-solving-based program invariant synthesis involves taking a parametric template, encoding the invariant conditions, and attempting to solve the constraints to obtain a valid assignment of parameters. The challenge lies in that the resulting constraints are often non-convex and lack efficient solvers. Consequently, existing works mostly rely on heuristic algorithms or general-purpose sol… ▽ More Constraint-solving-based program invariant synthesis involves taking a parametric template, encoding the invariant conditions, and attempting to solve the constraints to obtain a valid assignment of parameters. The challenge lies in that the resulting constraints are often non-convex and lack efficient solvers. Consequently, existing works mostly rely on heuristic algorithms or general-purpose solvers, leading to a trade-off between completeness and efficiency. In this paper, we propose two novel approaches to synthesize invariants for polynomial programs using semidefinite programming (SDP). For basic semialgebraic templates, we apply techniques from robust optimization to construct a hierarchy of SDP relaxations. These relaxations induce a series of sub-level sets that under-approximate the set of valid parameter assignments. Under a certain non-degenerate assumption, we present a weak completeness result that the synthesized sets include almost all valid assignments. Furthermore, we discuss several extensions to improve the efficiency and expressiveness of the algorithm. We also identify a subclass of basic semialgebraic templates, called masked templates, for which the non-degenerate assumption is violated. Regarding masked templates, we present a substitution-based method to strengthen the invariant conditions. The strengthened constraints again admit a hierarchy of SDP approximations. Both of our approaches have been implemented, and empirical results demonstrate that they outperform the state-of-the-art methods. △ Less

Submitted 17 October, 2023; originally announced October 2023.

Comments: 26 pages, 4 figures, in submission

ACM Class: F.3.1; G.1.6

A Generalized Hybrid Hoare Logic

Authors: Naijun Zhan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Dimitar Guelev

Abstract: Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by concurrent processes that communicate with each other. However, existing specification logics cannot easily handle such models. In this paper, we present a spec… ▽ More Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by concurrent processes that communicate with each other. However, existing specification logics cannot easily handle such models. In this paper, we present a specification logic and proof system for Hybrid Communicating Sequential Processes (HCSP), that extends CSP with ordinary differential equations (ODE) and interrupts to model interactions between continuous and discrete evolution. Because it includes a rich set of algebraic operators, complicated hybrid systems can be easily modelled in an algebra-like compositional way in HCSP. Our logic can be seen as a generalization and simplification of existing hybrid Hoare logics (HHL) based on duration calculus (DC), as well as a conservative extension of existing Hoare logics for concurrent programs. Its assertion logic is the first-order theory of differential equations (FOD), together with assertions about traces recording communications, readiness, and continuous evolution. We prove continuous relative completeness of the logic w.r.t. FOD, as well as discrete relative completeness in the sense that continuous behaviour can be arbitrarily approximated by discretization. Finally, we implement the above logic in Isabelle/HOL, and apply it to verify two case studies to illustrate the power and scalability of our logic. △ Less

Submitted 13 July, 2024; v1 submitted 27 March, 2023; originally announced March 2023.

Lower Bounds for Possibly Divergent Probabilistic Programs

Authors: Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan

Abstract: We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the case for existing rules -- and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional r… ▽ More We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the case for existing rules -- and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice. △ Less

Submitted 12 February, 2023; originally announced February 2023.

Comments: Paper conditionally accepted by OOPSLA 2023

Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming

Authors: Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen

Abstract: A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid systems possibly over an infinite time horizon. We present a novel condition on barrier certificates, termed the invariant barrier-certificate condition, that witnesses unbounded-time safety of differential dynamical syst… ▽ More A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid systems possibly over an infinite time horizon. We present a novel condition on barrier certificates, termed the invariant barrier-certificate condition, that witnesses unbounded-time safety of differential dynamical systems. The proposed condition is the weakest possible one to attain inductive invariance. We show that discharging the invariant barrier-certificate condition -- thereby synthesizing invariant barrier certificates -- can be encoded as solving an optimization problem subject to bilinear matrix inequalities (BMIs). We further propose a synthesis algorithm based on difference-of-convex programming, which approaches a local optimum of the BMI problem via solving a series of convex optimization problems. This algorithm is incorporated in a branch-and-bound framework that searches for the global optimum in a divide-and-conquer fashion. We present a weak completeness result of our method, namely, a barrier certificate is guaranteed to be found (under some mild assumptions) whenever there exists an inductive invariant (in the form of a given template) that suffices to certify safety of the system. Experimental results on benchmarks demonstrate the effectiveness and efficiency of our approach. △ Less

Submitted 20 September, 2022; originally announced September 2022.

Comments: To be published in Inf. Comput. arXiv admin note: substantial text overlap with arXiv:2105.14311

Machine-checked executable semantics of Stateflow

Authors: Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan

Abstract: Simulink is a widely used model-based development environment for embedded systems. Stateflow is a component of Simulink for modeling event-driven control via hierarchical state machines and flow charts. However, Stateflow lacks an official formal semantics, making it difficult to formally prove properties of its models in safety-critical applications. In this paper, we define a formal semantics f… ▽ More Simulink is a widely used model-based development environment for embedded systems. Stateflow is a component of Simulink for modeling event-driven control via hierarchical state machines and flow charts. However, Stateflow lacks an official formal semantics, making it difficult to formally prove properties of its models in safety-critical applications. In this paper, we define a formal semantics for a large subset of Stateflow, covering complex features such as hierarchical states and transitions, event broadcasts, early return, temporal operators, and so on. The semantics is formalized in Isabelle/HOL and proved to be deterministic. We implement a tactic for automatic execution of the semantics in Isabelle, as well as a translator in Python transforming Stateflow models to the syntax in Isabelle. Using these tools, we validate the semantics against a collection of examples illustrating the features we cover. △ Less

Submitted 25 July, 2022; originally announced July 2022.

Comments: 26 pages

Defensive Design of Saturating Counters Based on Differential Privacy

Authors: Depeng Liu, Lutan Zhao, Pengfei Yang, Bow-Yaw Wang, Rui Hou, Lijun Zhang, Naijun Zhan

Abstract: The saturating counter is the basic module of the dynamic branch predictor, which involves the core technique to improve instruction level parallelism performance in modern processors. However, most studies focus on the performance improvement and hardware consumption of saturating counters, while ignoring the security problems they may cause. In this paper, we creatively propose to study and desi… ▽ More The saturating counter is the basic module of the dynamic branch predictor, which involves the core technique to improve instruction level parallelism performance in modern processors. However, most studies focus on the performance improvement and hardware consumption of saturating counters, while ignoring the security problems they may cause. In this paper, we creatively propose to study and design saturating counters from the defense perspective of differential privacy, so that attackers cannot distinguish the states that saturating counters are in and further infer sensitive information. To obtain theoretical guarantees, we use Markov chain to formalize the attack algorithm applied to the saturating counter, investigate into the optimal attack strategy and calculate the probability of successful attack. Furthermore, we find that the attacker is able to accurately guess the branch execution of the victim's process in the existing saturating counters. To avoid this, we design a new probabilistic saturating counter, which generalizes the existing conventional and probabilistic saturating counters. The guarantee of differential privacy is applied to deduce parameters of the new saturating counters so that the security requirement can be satisfied. We also theoretically calculate the misprediction rate when the saturating counter reaches the steady state. The experimental results on testing programs show that the calculated theoretical results agree with the experimental performances. Compared with the existing conventional and probabilistic saturating counters, when the parameters of our designed models are selected appropriately, the new saturating counters can not only ensure similar operational performance, but also establish strict security guarantee. △ Less

Submitted 1 June, 2022; originally announced June 2022.

Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming

Authors: Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen

Abstract: A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid systems possibly over the infinite time horizon. We present a novel condition on barrier certificates, termed the invariant barrier-certificate condition, that witnesses unbounded-time safety of differential dynamical sys… ▽ More A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid systems possibly over the infinite time horizon. We present a novel condition on barrier certificates, termed the invariant barrier-certificate condition, that witnesses unbounded-time safety of differential dynamical systems. The proposed condition is by far the least conservative one on barrier certificates, and can be shown as the weakest possible one to attain inductive invariance. We show that discharging the invariant barrier-certificate condition -- thereby synthesizing invariant barrier certificates -- can be encoded as solving an optimization problem subject to bilinear matrix inequalities (BMIs). We further propose a synthesis algorithm based on difference-of-convex programming, which approaches a local optimum of the BMI problem via solving a series of convex optimization problems. This algorithm is incorporated in a branch-and-bound framework that searches for the global optimum in a divide-and-conquer fashion. We present a weak completeness result of our method, in the sense that a barrier certificate is guaranteed to be found (under some mild assumptions) whenever there exists an inductive invariant (in the form of a given template) that suffices to certify safety of the system. Experimental results on benchmark examples demonstrate the effectiveness and efficiency of our approach. △ Less

Submitted 29 May, 2021; originally announced May 2021.

Comments: To be published in Proc. of CAV 2021

Where does the Stimulus go? Deep Generative Model for Commercial Banking Deposits

Authors: Ni Zhan

Abstract: This paper examines deposits of individuals ("retail") and large companies ("wholesale") in the U.S. banking industry, and how these deposit types are impacted by macroeconomic factors, such as quantitative easing (QE). Actual data for deposits by holder are unavailable. We use a dataset on banks' financial information and probabilistic generative model to predict industry retail-wholesale deposit… ▽ More This paper examines deposits of individuals ("retail") and large companies ("wholesale") in the U.S. banking industry, and how these deposit types are impacted by macroeconomic factors, such as quantitative easing (QE). Actual data for deposits by holder are unavailable. We use a dataset on banks' financial information and probabilistic generative model to predict industry retail-wholesale deposit split from 2000 to 2020. Our model assumes account balances arise from separate retail and wholesale lognormal distributions and fit parameters of distributions by minimizing error between actual bank metrics and simulated metrics using the model's generative process. We use time-series regression to forward predict retail-wholesale deposits as function of loans, retail loans, and reserve balances at Fed banks. We find increase in reserves (representing QE) increases wholesale but not retail deposits, and increase in loans increase both wholesale and retail deposits evenly. The result shows that QE following the 2008 financial crisis benefited large companies more than average individuals, a relevant finding for economic decision making. In addition, this work benefits bank management strategy by providing forecasting capability for retail-wholesale deposits. △ Less

Submitted 22 January, 2021; originally announced January 2021.

Journal ref: NeurIPS 2020 workshop on ML for Economic Policy

Graphical Models for Financial Time Series and Portfolio Selection

Authors: Ni Zhan, Yijia Sun, Aman Jakhar, He Liu

Abstract: We examine a variety of graphical models to construct optimal portfolios. Graphical models such as PCA-KMeans, autoencoders, dynamic clustering, and structural learning can capture the time varying patterns in the covariance matrix and allow the creation of an optimal and robust portfolio. We compared the resulting portfolios from the different models with baseline methods. In many cases our graph… ▽ More We examine a variety of graphical models to construct optimal portfolios. Graphical models such as PCA-KMeans, autoencoders, dynamic clustering, and structural learning can capture the time varying patterns in the covariance matrix and allow the creation of an optimal and robust portfolio. We compared the resulting portfolios from the different models with baseline methods. In many cases our graphical strategies generated steadily increasing returns with low risk and outgrew the S&P 500 index. This work suggests that graphical models can effectively learn the temporal dependencies in time series data and are proved useful in asset management. △ Less

Submitted 22 January, 2021; originally announced January 2021.

Comments: Published at ACM International Conference on AI in Finance (ICAIF '20)

Learning One-Clock Timed Automata

Authors: Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang

Abstract: We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin's $L^*$ algorithm and inspired by existing work on the active learning of symbolic automata. Due to the need of guessing for each transition whether it resets the clock, the algorithm is of exponential complexity in the size of the learned automata. Befo… ▽ More We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin's $L^*$ algorithm and inspired by existing work on the active learning of symbolic automata. Due to the need of guessing for each transition whether it resets the clock, the algorithm is of exponential complexity in the size of the learned automata. Before presenting this algorithm, we propose a simpler version where the teacher is assumed to be smart in the sense of being able to provide the reset information. We show that this simpler setting yields a polynomial complexity of the learning process. Both of the algorithms are implemented and evaluated on a collection of randomly generated examples. We furthermore demonstrate the simpler algorithm on the functional specification of the TCP protocol. △ Less

Submitted 26 March, 2020; v1 submitted 23 October, 2019; originally announced October 2019.

Comments: Full version of the paper in TACAS2020

NIL: Learning Nonlinear Interpolants

Authors: Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan

Abstract: Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model checking, abstract interpretation, etc. The underlying synthesis problem, however, is challenging and existing methods have limitations on the form of formulae to be interpolated. We leverage classification techniques with space transformations and kernel tricks a… ▽ More Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model checking, abstract interpretation, etc. The underlying synthesis problem, however, is challenging and existing methods have limitations on the form of formulae to be interpolated. We leverage classification techniques with space transformations and kernel tricks as established in the realm of machine learning, and present a counterexample-guided method named NIL for synthesizing polynomial interpolants, thereby yielding a unified framework tackling the interpolation problem for the general quantifier-free theory of nonlinear arithmetic, possibly involving transcendental functions. We prove the soundness of NIL and propose sufficient conditions under which NIL is guaranteed to converge, i.e., the derived sequence of candidate interpolants converges to an actual interpolant, and is complete, namely the algorithm terminates by producing an interpolant if there exists one. The applicability and effectiveness of our technique are demonstrated experimentally on a collection of representative benchmarks from the literature, where in particular, our method suffices to address more interpolation tasks, including those with perturbations in parameters, and in many cases synthesizes simpler interpolants compared with existing approaches. △ Less

Submitted 28 August, 2019; v1 submitted 28 May, 2019; originally announced May 2019.

Comments: Full version of the paper in Proc. of CADE-27, with typos corrected

Nonlinear Craig Interpolant Generation

Authors: Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, Liyun Dai

Abstract: Interpolation-based techniques have become popularized in recent years because of their inherently modular and local reasoning, which can scale up existing formal verification techniques like theorem proving, model-checking, abstraction interpretation, and so on, while the scalability is the bottleneck of these techniques. Craig interpolant generation plays a central role in interpolation-based te… ▽ More Interpolation-based techniques have become popularized in recent years because of their inherently modular and local reasoning, which can scale up existing formal verification techniques like theorem proving, model-checking, abstraction interpretation, and so on, while the scalability is the bottleneck of these techniques. Craig interpolant generation plays a central role in interpolation-based techniques, and therefore has drawn increasing attentions. In the literature, there are various works done on how to automatically synthesize interpolants for decidable fragments of first-order logic, linear arithmetic, array logic, equality logic with uninterpreted functions (EUF), etc., and their combinations. But Craig interpolant generation for non-linear theory and its combination with the aforementioned theories are still in infancy, although some attempts have been done. In this paper, we first prove that a polynomial interpolant of the form $h(\mathbf{x})>0$ exists for two mutually contradictory polynomial formulas $φ(\mathbf{x},\mathbf{y})$ and $ψ(\mathbf{x},\mathbf{z})$, with the form $f_1\ge0\wedge\cdots\wedge f_n\ge0$, where $f_i$ are polynomials in $\mathbf{x},\mathbf{y}$ or $\mathbf{x},\mathbf{z}$, and the quadratic module generated by $f_i$ is Archimedean. Then, we show that synthesizing such interpolant can be reduced to solving a semi-definite programming problem (${\rm SDP}$). In addition, we propose a verification approach to assure the validity of the synthesized interpolant and consequently avoid the unsoundness caused by numerical error in ${\rm SDP}$ solving. Finally, we discuss how to generalize our approach to general semi-algebraic formulas. △ Less

Submitted 10 May, 2020; v1 submitted 4 March, 2019; originally announced March 2019.

Comments: 32 pages, 4 figures

Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems

Authors: Bai Xue, Naijun Zhan

Abstract: In this paper we study the robust invariant sets generation problem for discrete-time switched polynomial systems subject to disturbance inputs within the optimal control framework. A robust invariant set of interest is a set of states such that every possible trajectory starting from it never leaves a specified safe set, regardless of actual disturbances. The maximal robust invariant set is shown… ▽ More In this paper we study the robust invariant sets generation problem for discrete-time switched polynomial systems subject to disturbance inputs within the optimal control framework. A robust invariant set of interest is a set of states such that every possible trajectory starting from it never leaves a specified safe set, regardless of actual disturbances. The maximal robust invariant set is shown to be the zero level set of the unique bounded solution to a Bellman type equation, which is a functional equation being widely used in discrete-time optimal control. This is the main contribution of this work. The uniqueness of bounded solutions enables us to solve the derived Bellman type equation using numerical methods such as the value iteration, which provides an approximation of the maximal robust invariant set. In order to increase the scalability of the Bellman equation based method, a semi-definite program, which is constructed based on the derived Bellman type equation, is also implemented to synthesize robust invariant sets. Finally, three examples demonstrate the performance of our methods. △ Less

Submitted 19 March, 2021; v1 submitted 28 November, 2018; originally announced November 2018.

Comments: This paper is accepted by IEEE TAC. The title is changed to 'Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems'

Parameter Synthesis Problems for one parametric clock Timed Automata

Authors: Liyun Dai, Taolue Chen, Zhiming Liu, Bican Xia, Naijun Zhan, Kim G. Larsen

Abstract: In this paper, we study the parameter synthesis problem for a class of parametric timed automata. The problem asks to construct the set of valuations of the parameters in the parametric timed automa- ton, referred to as the feasible region, under which the resulting timed automaton satisfies certain properties. We show that the parameter syn- thesis problem of parametric timed automata with only o… ▽ More In this paper, we study the parameter synthesis problem for a class of parametric timed automata. The problem asks to construct the set of valuations of the parameters in the parametric timed automa- ton, referred to as the feasible region, under which the resulting timed automaton satisfies certain properties. We show that the parameter syn- thesis problem of parametric timed automata with only one parametric clock (unlimited concretely constrained clock) and arbitrarily many pa- rameters is solvable when all the expressions are linear expressions. And it is moreover the synthesis problem is solvable when the form of con- straints are parameter polynomial inequality not just simple constraint and parameter domain is nonnegative real number. △ Less

Submitted 15 September, 2018; originally announced September 2018.

Comments: 20 pages, 1 figure. arXiv admin note: substantial text overlap with arXiv:1808.06792

Triplet-based Deep Similarity Learning for Person Re-Identification

Authors: Wentong Liao, Michael Ying Yang, Ni Zhan, Bodo Rosenhahn

Abstract: In recent years, person re-identification (re-id) catches great attention in both computer vision community and industry. In this paper, we propose a new framework for person re-identification with a triplet-based deep similarity learning using convolutional neural networks (CNNs). The network is trained with triplet input: two of them have the same class labels and the other one is different. It… ▽ More In recent years, person re-identification (re-id) catches great attention in both computer vision community and industry. In this paper, we propose a new framework for person re-identification with a triplet-based deep similarity learning using convolutional neural networks (CNNs). The network is trained with triplet input: two of them have the same class labels and the other one is different. It aims to learn the deep feature representation, with which the distance within the same class is decreased, while the distance between the different classes is increased as much as possible. Moreover, we trained the model jointly on six different datasets, which differs from common practice - one model is just trained on one dataset and tested also on the same one. However, the enormous number of possible triplet data among the large number of training samples makes the training impossible. To address this challenge, a double-sampling scheme is proposed to generate triplets of images as effective as possible. The proposed framework is evaluated on several benchmark datasets. The experimental results show that, our method is effective for the task of person re-identification and it is comparable or even outperforms the state-of-the-art methods. △ Less

Submitted 9 February, 2018; originally announced February 2018.

Comments: ICCV Workshops 2017

Synthesizing SystemC Code from Delay Hybrid CSP

Authors: Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan

Abstract: Delay is omnipresent in modern control systems, which can prompt oscillations and may cause deterioration of control performance, invalidate both stability and safety properties. This implies that safety or stability certificates obtained on idealized, delay-free models of systems prone to delayed coupling may be erratic, and further the incorrectness of the executable code generated from these mo… ▽ More Delay is omnipresent in modern control systems, which can prompt oscillations and may cause deterioration of control performance, invalidate both stability and safety properties. This implies that safety or stability certificates obtained on idealized, delay-free models of systems prone to delayed coupling may be erratic, and further the incorrectness of the executable code generated from these models. However, automated methods for system verification and code generation that ought to address models of system dynamics reflecting delays have not been paid enough attention yet in the computer science community. In our previous work, on one hand, we investigated the verification of delay dynamical and hybrid systems; on the other hand, we also addressed how to synthesize SystemC code from a verified hybrid system modelled by Hybrid CSP (HCSP) without delay. In this paper, we give a first attempt to synthesize SystemC code from a verified delay hybrid system modelled by Delay HCSP (dHCSP), which is an extension of HCSP by replacing ordinary differential equations (ODEs) with delay differential equations (DDEs). We implement a tool to support the automatic translation from dHCSP to SystemC. △ Less

Submitted 19 September, 2017; originally announced September 2017.

Finding polynomial loop invariants for probabilistic programs

Authors: Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia

Abstract: Quantitative loop invariants are an essential element in the verification of probabilistic programs. Recently, multivariate Lagrange interpolation has been applied to synthesizing polynomial invariants. In this paper, we propose an alternative approach. First, we fix a polynomial template as a candidate of a loop invariant. Using Stengle's Positivstellensatz and a transformation to a sum-of-square… ▽ More Quantitative loop invariants are an essential element in the verification of probabilistic programs. Recently, multivariate Lagrange interpolation has been applied to synthesizing polynomial invariants. In this paper, we propose an alternative approach. First, we fix a polynomial template as a candidate of a loop invariant. Using Stengle's Positivstellensatz and a transformation to a sum-of-squares problem, we find sufficient conditions on the coefficients. Then, we solve a semidefinite programming feasibility problem to synthesize the loop invariants. If the semidefinite program is unfeasible, we backtrack after increasing the degree of the template. Our approach is semi-complete in the sense that it will always lead us to a feasible solution if one exists and numerical errors are small. Experimental results show the efficiency of our approach. △ Less

Submitted 10 July, 2017; originally announced July 2017.

Comments: accompanies an ATVA 2017 submission

Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus

Authors: Dimitar Guelev, Shuling Wang, Naijun Zhan

Abstract: Deductive methods for the verification of hybrid systems vary on the format of statements in correctness proofs. Building on the example of Hoare triple-based reasoning, we have investigated several such methods for systems described in Hybrid CSP, each based on a different assertion language, notation for time, and notation for proofs, and each having its pros and cons with respect to expressive… ▽ More Deductive methods for the verification of hybrid systems vary on the format of statements in correctness proofs. Building on the example of Hoare triple-based reasoning, we have investigated several such methods for systems described in Hybrid CSP, each based on a different assertion language, notation for time, and notation for proofs, and each having its pros and cons with respect to expressive power, compositionality and practical convenience. In this paper we propose a new approach based on weakly monotonic time as the semantics for interleaving, the Duration Calculus (DC) with infinite intervals and general fixpoints as the logic language, and a new meaning for Hoare-like triples which unifies assertions and temporal conditions. We include a proof system for reasoning about the properties of systems written in the new form of triples that is complete relative to validity in DC. △ Less

Submitted 27 June, 2017; v1 submitted 19 June, 2017; originally announced June 2017.

Approximate Bisimulation and Discretization of Hybrid CSP

Authors: Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan

Abstract: Hybrid Communicating Sequential Processes (HCSP) is a powerful formal modeling language for hybrid systems, which is an extension of CSP by introducing differential equations for modeling continuous evolution and interrupts for modeling interaction between continuous and discrete dynamics. In this paper, we investigate the semantic foundation for HCSP from an operational point of view by proposing… ▽ More Hybrid Communicating Sequential Processes (HCSP) is a powerful formal modeling language for hybrid systems, which is an extension of CSP by introducing differential equations for modeling continuous evolution and interrupts for modeling interaction between continuous and discrete dynamics. In this paper, we investigate the semantic foundation for HCSP from an operational point of view by proposing notion of approximate bisimulation, which provides an appropriate criterion to characterize the equivalence between HCSP processes with continuous and discrete behaviour. We give an algorithm to determine whether two HCSP processes are approximately bisimilar. In addition, based on that, we propose an approach on how to discretize HCSP, i.e., given an HCSP process A, we construct another HCSP process B which does not contain any continuous dynamics such that A and B are approximately bisimilar with given precisions. This provides a rigorous way to transform a verified control model to a correct program model, which fills the gap in the design of embedded systems. △ Less

Submitted 7 September, 2016; v1 submitted 31 August, 2016; originally announced September 2016.

Comments: FM 2016, Proof Appendix, HCSP, approximately bisimilar, hybrid systems, discretization

Interpolation synthesis for quadratic polynomial inequalities and combination with EUF

Authors: Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen

Abstract: An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and nonstrict) is proposed. The algorithm is based on a key observation that quadratic polynomial inequalities can be linearized if they are concave. A generalization of Motzkin's transposition theorem is proved, which is used to generate an interpolant between two mutuall… ▽ More An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and nonstrict) is proposed. The algorithm is based on a key observation that quadratic polynomial inequalities can be linearized if they are concave. A generalization of Motzkin's transposition theorem is proved, which is used to generate an interpolant between two mutually contradictory conjunctions of polynomial inequalities, using semi-definite programming in time complexity $\mathcal{O}(n^3+nm))$, where $n$ is the number of variables and $m$ is the number of inequalities. Using the framework proposed by \cite{SSLMCS2008} for combining interpolants for a combination of quantifier-free theories which have their own interpolation algorithms, a combination algorithm is given for the combined theory of concave quadratic polynomial inequalities and the equality theory over uninterpreted functions symbols (\textit{EUF}). The proposed approach is applicable to all existing abstract domains like \emph{octagon}, \emph{polyhedra}, \emph{ellipsoid} and so on, therefore it can be used to improve the scalability of existing verification techniques for programs and hybrid systems. In addition, we also discuss how to extend our approach to formulas beyond concave quadratic polynomials using Gröbner basis. △ Less

Submitted 10 November, 2016; v1 submitted 19 January, 2016; originally announced January 2016.

Comments: 40 pages, 1 figures

ACM Class: D.2.4

A Theorem Prover for Quantum Hoare Logic and Its Applications

Authors: Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, Naijun Zhan

Abstract: Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs. In this paper, we implement a theorem prover for QHL based on Isabelle/HOL. By applying the theorem prover, verifying a quantum program against a specification is transformed equivalently into an order relation between matrices. Due to the limitation of Isabelle/HOL, the calculation of the order r… ▽ More Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs. In this paper, we implement a theorem prover for QHL based on Isabelle/HOL. By applying the theorem prover, verifying a quantum program against a specification is transformed equivalently into an order relation between matrices. Due to the limitation of Isabelle/HOL, the calculation of the order relation is solved by calling an outside oracle written in Python. To the best of our knowledge, this is the first theorem prover for quantum programs. To demonstrate its power, the correctness of two well-known quantum algorithms, i.e., Grover Quantum Search and Quantum Phase Estimation (the key step in Shor's quantum algorithm of factoring in polynomial time) are proved using the theorem prover. These are the first mechanized proofs for both of them. △ Less

Submitted 15 January, 2016; originally announced January 2016.

On Termination of Polynomial Programs with Equality Conditions

Authors: Yangjia Li, Naijun Zhan, Mingshuai Chen, Hui Lu, Guohua Wu, Joost-Pieter Katoen

Abstract: We investigate the termination problem of a family of multi-path polynomial programs (MPPs), in which all assignments to program variables are polynomials, and test conditions of loops and conditional statements are polynomial equalities. We show that the set of non-terminating inputs (NTI) of such a program is algorithmically computable, thus leading to the decidability of its termination. To the… ▽ More We investigate the termination problem of a family of multi-path polynomial programs (MPPs), in which all assignments to program variables are polynomials, and test conditions of loops and conditional statements are polynomial equalities. We show that the set of non-terminating inputs (NTI) of such a program is algorithmically computable, thus leading to the decidability of its termination. To the best of our knowledge, the considered family of MPPs is hitherto the largest one for which termination is decidable. We present an explicit recursive function which is essentially Ackermannian, to compute the maximal length of ascending chains of polynomial ideals under a control function, and thereby obtain a complete answer to the questions raised by Seidenberg. This maximal length facilitates a precise complexity analysis of our algorithms for computing the NTI and deciding termination of MPPs. We extend our method to programs with polynomial guarded commands and show how an incomplete procedure for MPPs with inequality guards can be obtained. An application of our techniques to invariant generation of polynomial programs is further presented. △ Less

Submitted 1 September, 2020; v1 submitted 18 October, 2015; originally announced October 2015.

MSC Class: 68Q60 (Primary) 68W30; 68Q17 (Secondary)

Extending Hybrid CSP with Probability and Stochasticity

Authors: Yu Peng, Shuling Wang, Naijun Zhan, Lijun Zhang

Abstract: Probabilistic and stochastic behavior are omnipresent in computer controlled systems, in particular, so-called safety-critical hybrid systems, because of fundamental properties of nature, uncertain environments, or simplifications to overcome complexity. Tightly intertwining discrete, continuous and stochastic dynamics complicates modelling, analysis and verification of stochastic hybrid systems (… ▽ More Probabilistic and stochastic behavior are omnipresent in computer controlled systems, in particular, so-called safety-critical hybrid systems, because of fundamental properties of nature, uncertain environments, or simplifications to overcome complexity. Tightly intertwining discrete, continuous and stochastic dynamics complicates modelling, analysis and verification of stochastic hybrid systems (SHSs). In the literature, this issue has been extensively investigated, but unfortunately it still remains challenging as no promising general solutions are available yet. In this paper, we give our effort by proposing a general compositional approach for modelling and verification of SHSs. First, we extend Hybrid CSP (HCSP), a very expressive and process algebra-like formal modeling language for hybrid systems, by introducing probability and stochasticity to model SHSs, which is called stochastic HCSP (SHCSP). To this end, ordinary differential equations (ODEs) are generalized by stochastic differential equations (SDEs) and non-deterministic choice is replaced by probabilistic choice. Then, we extend Hybrid Hoare Logic (HHL) to specify and reason about SHCSP processes. We demonstrate our approach by an example from real-world. △ Less

Submitted 4 September, 2015; originally announced September 2015.

Comments: The conference version of this paper is accepted by SETTA 2015

Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation

Authors: Deepak Kapur, Naijun Zhan, Hengjun Zhao

Abstract: We extend a template-based approach for synthesizing switching controllers for semi-algebraic hybrid systems, in which all expressions are polynomials. This is achieved by combining a QE (quantifier elimination)-based method for generating continuous invariants with a qualitative approach for predefining templates. Our synthesis method is relatively complete with regard to a given family of predef… ▽ More We extend a template-based approach for synthesizing switching controllers for semi-algebraic hybrid systems, in which all expressions are polynomials. This is achieved by combining a QE (quantifier elimination)-based method for generating continuous invariants with a qualitative approach for predefining templates. Our synthesis method is relatively complete with regard to a given family of predefined templates. Using qualitative analysis, we discuss heuristics to reduce the numbers of parameters appearing in the templates. To avoid too much human interaction in choosing templates as well as the high computational complexity caused by QE, we further investigate applications of the SOS (sum-of-squares) relaxation approach and the template polyhedra approach in continuous invariant generation, which are both well supported by efficient numerical solvers. △ Less

Submitted 2 April, 2013; originally announced April 2013.

Generating Non-Linear Interpolants by Semidefinite Programming

Authors: Liyun Dai, Bican Xia, Naijun Zhan

Abstract: Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model check- ing, CEGAR, SMT, etc., whose hardest part is how to synthesize interpolants. Various work for discovering interpolants for propositional logic, quantifier-free fragments of first-order theories and their combinations have been proposed. However, littl… ▽ More Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model check- ing, CEGAR, SMT, etc., whose hardest part is how to synthesize interpolants. Various work for discovering interpolants for propositional logic, quantifier-free fragments of first-order theories and their combinations have been proposed. However, little work focuses on discovering polynomial interpolants in the literature. In this paper, we provide an approach for constructing non-linear interpolants based on semidefinite programming, and show how to apply such results to the verification of programs by examples. △ Less

Submitted 3 March, 2013; v1 submitted 18 February, 2013; originally announced February 2013.

Comments: 22 pages, 4 figures

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example

Authors: Hengjun Zhao, Naijun Zhan, Deepak Kapur, Kim G. Larsen

Abstract: In this paper, we propose an approach to reduce the optimal controller synthesis problem of hybrid systems to quantifier elimination; furthermore, we also show how to combine quantifier elimination with numerical computation in order to make it more scalable but at the same time, keep arising errors due to discretization manageable and within bounds. A major advantage of our approach is not only t… ▽ More In this paper, we propose an approach to reduce the optimal controller synthesis problem of hybrid systems to quantifier elimination; furthermore, we also show how to combine quantifier elimination with numerical computation in order to make it more scalable but at the same time, keep arising errors due to discretization manageable and within bounds. A major advantage of our approach is not only that it avoids errors due to numerical computation, but it also gives a better optimal controller. In order to illustrate our approach, we use the real industrial example of an oil pump provided by the German company HYDAC within the European project Quasimodo as a case study throughout this paper, and show that our method improves (up to 7.5%) the results reported in [3] based on game theory and model checking. △ Less

Submitted 2 June, 2012; v1 submitted 26 March, 2012; originally announced March 2012.

Computing Semi-algebraic Invariants for Polynomial Dynamical Systems

Authors: Jiang Liu, Naijun Zhan, Hengjun Zhao

Abstract: In this paper, we consider an extended concept of invariant for polynomial dynamical system (PDS) with domain and initial condition, and establish a sound and complete criterion for checking semi-algebraic invariants (SAI) for such PDSs. The main idea is encoding relevant dynamical properties as conditions on the high order Lie derivatives of polynomials occurring in the SAI. A direct consequence… ▽ More In this paper, we consider an extended concept of invariant for polynomial dynamical system (PDS) with domain and initial condition, and establish a sound and complete criterion for checking semi-algebraic invariants (SAI) for such PDSs. The main idea is encoding relevant dynamical properties as conditions on the high order Lie derivatives of polynomials occurring in the SAI. A direct consequence of this criterion is a relatively complete method of SAI generation based on template assumption and semi-algebraic constraint solving. Relative completeness means if there is an SAI in the form of a predefined template, then our method can indeed find one using this template. △ Less

Submitted 21 July, 2011; v1 submitted 3 February, 2011; originally announced February 2011.

Comments: 28 pages

ACM Class: I.1.2; D.2.4