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.

Home | Organization | Program | Submission | Registration | Accommodation

(Webmaster)

Home

Organization

Submission

Program

Registration

Accommodation

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