Efficient Constraint Solving Engines to Reason about Real Time Systems
Abstract
This proposal is concerned with certification in various constraint s ystems. In particular, we focus on constraint systems defined by systems of linear i nequalities. The constraint systems that we focus on, arise in real time system specifications. We explore the expressiveness scalability spectrum of formal models for real time systems between difference constraint supported timed automata and linear constraints supported (affine) hybrid a utomata. We argue for the existence of useful formalisms to model real time systems more expressive than timed automata that permit more scalable analysis than hybrid automata. To develop efficient constraint solving engines required to support robust analysis frameworks for such models beyond timed automata, we study decision procedures for a wide variety of constraint systems over both integers and reals. We study a spectrum of constraint systems between the difference constraint systems and linear constraint systems, ranging from unit two variables per inequality (UTVPI) constraint system to more general octahedral constraint systems.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 14, 2022
- Source ID
- FA95501910177
Entities
People
- Krishnamurthy Subramani
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- West Virginia University