Write a Blog >>
Wed 20 Jan 2016 15:10 - 15:35 at Grand Bay North - Track 1: Decision Procedures Chair(s): Loris D'Antoni

Ordinary differential equations (ODEs) are widespread in many natural sciences including chemistry, ecology, and systems biology, and in disciplines such as control theory and electrical engineering. Building on the celebrated molecules-as-processes paradigm, they have become increasingly popular in computer science, with high-level languages and formal methods such as Petri nets, process algebra, and rule-based systems that are interpreted as ODEs.

We consider the problem of comparing and minimizing ODEs automatically. Influenced by traditional approaches in the theory of programming, we propose differential equivalence relations. We study them for a basic intermediate language, for which we have decidability results, that can be targeted by a class of high-level specifications. An ODE implicitly represents an uncountable state space, hence reasoning techniques cannot be borrowed from established domains such as probabilistic programs with finite-state Markov chain semantics. Instead we provide novel procedures to check an equivalence and compute the largest one via partition refinement algorithms that use satisfiability modulo theories.

We illustrate the generality of our framework by showing that differential equivalences include (i) well-known notions for the minimization of continuous-time Markov chains (lumpability), (ii) bisimulations for chemical reaction networks recently proposed by Cardelli et al., and (iii) behavioral relations for process algebra with ODE semantics. With a prototype implementation we are able to detect equivalences in biochemical models from the literature that cannot be reduced using competing automatic techniques.

Wed 20 Jan
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

14:20 - 16:00: Research Papers - Track 1: Decision Procedures at Grand Bay North
Chair(s): Loris D'AntoniUniversity of Pennsylvania
POPL-2016-papers14:20 - 14:45
Xin ZhangGeorgia Tech, Ravi MangalGeorgia Institute of Technology, Aditya NoriMicrosoft Research, UK, Mayur NaikGeorgia Tech
File Attached
POPL-2016-papers14:45 - 15:10
Anthony Widjaja LinYale-NUS College, Singapore, Pablo BarceloUniversity of Chile, Chile
Media Attached
POPL-2016-papers15:10 - 15:35
Luca CardelliMicrosoft Research and University of Oxford, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy, Andrea VandinIMT Institute for Advanced Studies Lucca, Italy
Media Attached
POPL-2016-papers15:35 - 16:00
Matthew HagueRoyal Holloway University of London, UK, Jonathan KochemsDepartment of Computer Science, University of Oxford, C.-H. Luke OngUniversity of Oxford, UK
Media Attached