15 citations · 33 across the 13 of their papers we have counts for
13 papers
Solving Splitted Multi-Commodity Flow Problem by Efficient Linear Programming Algorithm
Liyun Dai, Hengjun Zhao, Zhiming Liu
Column generation is often used to solve multi-commodity flow problems. A program for column generation always includes a module that solves a linear equation. In this paper, we ad…
Online Observability of Boolean Control Networks
Guisen Wu, Liyun Dai, Zhiming Liu +2
Observabililty is an important topic of Boolean control networks (BCNs). In this paper, we propose a new type of observability named online observability to present the sufficient…
Nonlinear Craig Interpolant Generation
Ting Gan, Bican Xia, Bai Xue +2
Interpolation-based techniques have become popularized in recent years because of their inherently modular and local reasoning, which can scale up existing formal verification tech…
Parameter Synthesis Problems for one parametric clock Timed Automata
Liyun Dai, Taolue Chen, Zhiming Liu +3
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 param…
Parameter Synthesis Problems for Parametric Timed Automata
Liyun Dai, Bo Liu, Zhiming Liu +1
We consider the parameter synthesis problem of parametric timed automata (PTAs). The problem is, given a PTA and a property, to compute the set of valuations of the parameters unde…
Interpolation synthesis for quadratic polynomial inequalities and combination with EUF
Ting Gan, Liyun Dai, Bican Xia +3
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…
Open Weak CAD and its Applications
Jingjun Han, Liyun Dai, Hoon Hong +1
The concept of open weak CAD is introduced. Every open CAD is an open weak CAD. On the contrary, an open weak CAD is not necessarily an open CAD. An algorithm for computing project…
Smaller SDP for SOS Decomposition
Liyun Dai, Bican Xia
A popular numerical method to compute SOS (sum of squares of polynomials) decompositions for polynomials is to transform the problem into semi-definite programming (SDP) problems a…
Constructing Fewer Open Cells by GCD Computation in CAD Projection
Jingjun Han, Liyun Dai, Bican Xia
A new projection operator based on cylindrical algebraic decomposition (CAD) is proposed. The new operator computes the intersection of projection factor sets produced by different…
Barrier Certificates Revisited
Liyun Dai, Ting Gan, Bican Xia +1
A barrier certificate can separate the state space of a con- sidered hybrid system (HS) into safe and unsafe parts ac- cording to the safety property to be verified. Therefore this…
Generating Non-Linear Interpolants by Semidefinite Programming
Liyun Dai, Bican Xia, Naijun Zhan
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 ha…
logcf: An Efficient Tool for Real Root Isolation
Liyun Dai, Bican Xia
This paper revisits an algorithm for isolating real roots of univariate polynomials based on continued fractions. It follows the work of Vincent, Uspen- sky, Collins and Akritas, J…
Non-Termination Sets of Simple Linear Loops
Liyun Dai, Bican Xia
A simple linear loop is a simple while loop with linear assignments and linear loop guards. If a simple linear loop has only two program variables, we give a complete algorithm for…