Quasi-decidability and its Role in Hybrid Systems Verification

Stefan Ratschan

Institute of Computer Science, Academy of Sciences of the Czech Republic

Abstract

In the classical theory of computability, the notion of decidability was introduced to distinguish problems that are automatically solvable on computers from problems that are not. However, in recent years, several results appear that show that certain undecidable problems are quasi-decidable in the sense that they can be automatically solved on computers for all, but certain pathological problem instances. These are problem instances for which small changes in the problem description essentially change the result. We present several quasi-decidability results that we have proved in recent years, especially in the area of verification of hybrid systems, that is, dynamical systems that have both discrete and continuous state and evolution. These results have important practical consequences, since hybrid systems are an important formalism