A4 – Logic-Based Perspicuous Run-Time Supervision

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

Principal Investigator
Technische Universität Dresden
Principal Investigator
Technische Universität Dresden

Researchers

Martin Bromberger
( )
Rasha Faqeh
( , )
Lorenz Leutgeb
( )
Andre Martin
( )
Muhammad Usama Sardar
( , )
Uwe Waldmann
( )

Publications