with traditional methods would incur huge expression swell and high complexity. Indeed, many problems related to this one are provably intractable, or suspected to be so. Nonetheless, recent work has yielded exciting new algorithms for computing with sparse mathematical expressions. In this talk, we will attempt to navigate this hazardous computational terrain of sparse algebraic computation. We will discuss new algorithms for sparse polynomial root finding and functional decomposition. We will also look at the “inverse” problem of interpolating or reconstructing sparse mathematical functions from a small number of sample points. Computations over traditional symbolic domains, such as the integers and finite fields, as well as symbolic-numeric computations for approximate (floating point) data, will be considered. In all cases, algorithms will require time polynomial in the size of the sparse representation of the input and output, and will provably manage coefficient growth, intermediate expression swell, and numerical stability as appropriate to the problem.

Katsuhisa Horimoto

A constraint for optimal parameter estimation to solve an issue of molecular network models in systems biology

One point is definitely different between network modeling in systems biology and that in other scientific fields. The point is that the models including unmeasured variables frequently emerged, so as to measure the variables under the conditions with as less perturbation to the organism as possible. To consider the point specific to systems biology, we have designed a method by symbolic-computation approach, to estimate kinetic parameter values with a high degree of accuracy. First, we utilize differential elimination, which is an algebraic approach for rewriting a system of differential equations into another equivalent system, to derive the constraints between kinetic parameters from differential equations. Second, since its equivalent system is frequently composed of large equations, the system is further simplified by another symbolic computation. Third, we estimate the kinetic parameters introducing these constraints into an objective function, in addition to the error function of the square difference between the measured and estimated data, in the standard parameter optimization method such as the genetic algorithm (GA) and the particle swarm optimization (PSO). Here, the performance of our method for parameter accuracy improvement is illustrated by the simulation of two representative models in biology, a simple cascade model and a negative feedback model, and the actual data analysis for a signal transduction pathway, in comparison with the previous numerical methods. In addition, we will discuss the merits and pitfalls of the present method for further improvements.

Chaochen Zhou

Verifying programs with support from computer algebra

This talk is to report the recent achievements of our joint project in using Computer Algebra to verify software and hybrid systems. In the talk, we will explain the main ideas of a symbolic decision procedure for termination of linear programs, which can avoid rounding error leading to a wrong conclusion, a complete algorithm to generate semi-algebraic invariants for polynomial dynamical systems, and also a language and a calculus to model and verify hybrid systems based on the invariants.

Invited Speakers

Martin Fränzle

Engineering arithmetic constraint solvers for the analysis of hybrid discrete-continuous systems

Hybrid discrete-continuous dynamic behavior arises when discrete and continuous dynamic processes become connected, as in the case of embedded computers and their physical environment. An increasing number of the technical artifacts shaping our ambience are relying on embedded computer systems which do interact with their environment in a complex and often safety-critical manner, having sensitive variables of the environment in their sphere of control. Everyday examples include process control at all scales, ranging from household appliances to nuclear power plants, or embedded systems in the transportation domain, such as adaptive cruise control in automotive, aircraft collision avoidance protocols in avionics, or automatic train control applications, including the so-called moving-block principle allowing increased traffic density on high-speed tracks while ensuring collision avoidance.

Within this talk, we concentrate on automatic verification and analysis of such hybrid systems, with a focus on mixed numeric-symbolic methods manipulating both the discrete and the continuous state components symbolically by means of predicative encodings and dedicated constraint solvers. We provide a brief introduction to hybrid discrete-continuous systems, demonstrate the use of predicative encodings for concisely encoding operational high-level models, and continue to a set of constraint-based methods for automatically analyzing different classes of hybrid discrete-continuous dynamics. Covering the range from non-linear discrete-time hybrid systems to probabilistic hybrid systems, advanced arithmetic constraint solvers will be used as a workhorse for manipulating large and complex-structured Boolean combinations of arithmetic constraints arising in their analysis tasks.

Mark Giesbrecht

Sparsity and complexity in algebraic computation

Modern symbolic computation systems provide an expressive language for describing mathematical objects. For example, we can easily enter equations such as

into a computer algebra system. However, to determine the factorization

Wednesday, October 19

Thursday, October 20

Friday, October 21

Tentative Program

08:45-9:00

Opening

 

Session chair: Dongming Wang

09:00-10:00

Verifying programs with support from computer algebra
Chaochen Zhou

10:00-10:30

Coffee Break

 

Session chair: Naijun Zhan

10:30-11:00

Proving total correctness of loop programs via

symbolic-numeric computation method

Wang Lin, Min Wu, Zhengfeng Yang and Zhenbing Zeng

11:00-11:30

Superposition as a decision procedure for timed automata

Arnaud Fietzke and Christoph Weidenbach

11:30-12:00

An approach of modeling and analyzing data gathering protocol

Kang He, Hongli Yang, Zongyan Qiu and Meng Sun

12:00-12:30

The non-Archimedean theory of discrete systems

Vladimir Anashin

12:30-14:00

Lunch

 

Session chair: Marc Moreno Maza

14:00-14:30

Rational general solutions of trivariate rational systems of autonomous ODEs

Yanli Huang, L.X.Chau Ngo and Franz Winkler

14:30-15:00

Discovering polynomial Lyapunov functions

for continuous dynamical systems

Zhikun She, Haoyang Li and Bai Xue

15:00-15:30

Automatically discovering relaxed Lyapunov functions for

polynomial dynamical systems

Jiang Liu, Naijun Zhan and Hengjun Zhao

15:30-16:00

Coffee Break

 

Session chair: Katsuhisa Horimoto

16:00-16:30

Nonlinear analysis of a class of double saturated

polymolecular reversible biochemical reactions

Jinliang Wang, Jing He and Wei Feng

16:30-17:00

An efficient model predictive control with constraints

using a simple explicit control law

Yuhei Umeda and Hirokazu Anai

17:00-17:30

Diagonal interacting multiple model algorithm based on $H_\infty$ filtering

Xiaoyan Fu, Yingmin Jia and Cuiping Li      

18:00-20:00

Dinner

 

Session chair: Bican Xia

09:00-10:00

A constraint for optimal parameter estimation to solve an issue of molecular network models in systems

Katsuhisa Horimoto

10:00-10:30

Coffee Break

 

Session chair: Martin Fränzle

10:30-11:00

A coinductive calculus for QoS-aware

generic components composition

Luis S. Barbosa and Sun Meng

11:00-11:30

On the implementation of cubic public keys based on

algebraic graphs over the finite commutative ring

and their special symmetries

Michal Klisowski and Vasyl Ustimenko       

11:30-12:00

A New Family of p-ary Sequences with Low Correlation Constructed from Decimated Sequences

Yongbo Xia

12:00-12:30

Pre-Galois connection for generic state-based

components refinement

Sun Meng

12:30-14:00

Lunch

 

Session chair: Stefan Ratschan

14:00-15:00

Engineering arithmetic constraint solvers for the analysis of hybrid discrete-continuous systems

Martin Fränzle

15:00-15:30

C-XSC, a sophisticated environment for reliable computing

Walter Krämer

15:30-18:30

Excursion to Prince Gong's Mansion and Shicha Lake

19:00-21:30

Banquet

 

Session chair: Lihong Zhi

09:00-10:00

Sparsity and complexity in algebraic computation

Mark Giesbrecht

10:00-10:30

Coffee Break

 

Session chair: Marc Giusti

10:30-11:00

Solving semi-algebraic systems with the

RegularChains library in Maple

Changbo Chen, James Davenport, François Lemaire, Marc Moreno Maza,  Nalina Phisanbut, Bican Xia,

Rong Xiao and Yuzhen Xie

11:00-11:30

Improved bounds for continued fractions variants

for real root isolation

Elias Tsigaridas

11:30-12:00

The irreducibility of polynomials with coefficients in a

unique factorization domain

He Miao, Li Yongbin and He Cong

12:00-12:30

SUP(T) decides first-order logic fragment over ground theories

Evgeny Kruglov and Christoph Weidenbach

12:30-14:00

Lunch

 

Session chair: Mark Giesbrecht

14:00-14:30

Solving curve completion problems with discrete invariants

Jun Zhao and Elizabeth Mansfield

14:30-15:00

Point searching in real singular complete

intersection varieties – algorithms of intrinsic complexity

Bernd Bank, Marc Giusti and Joos Heintz

15:00-15:30

On solving parametric polynomial systems

Marc Moreno Maza, Bican Xia and Rong Xiao

15:30-16:00

Closing

18:00-20:00

Dinner