This project investigates perspicuous supervision of technical systems, carried out in a read data—analyse—react loop (RAR loop) several times per second. Our vision is a supervisor implemented by logical rules (clauses) out of a dedicated logical fragment, constituting a paradigm shift where (i) the declarative representation and formal logical reasoning provides explications, turning what is now a black box into a perspicuous system; (ii) testing can be replaced by automatic verification; (iii) the verified clauses can be deployed in a RAR loop; and as a consequence (iv) the overall product cycle is less costly. To these ends, we will investigate logical fragments combining (decidable) first-order logic fragments, representing control aspects, with (decidable) arithmetic theories, representing the abstraction of real-world technical system behaviour.
Project A4 has been completed at the end of the first funding phase.
Principal Investigators
