For slides, future Logic events and more, please visit: https://logic-data-science.github.io/?page=logic_learning
Two known shortcomings of standard techniques in formal verification are the limited capability to provide system-level assertions, and the scalability to large-scale, complex models, such as those needed in Cyber-Physical Systems (CPS) applications. This talk covers research which addresses these shortcomings, by bringing model-based and data-driven methods together, which can help pushing the envelope of existing algorithms and tools in formal verification.
In the first part of the talk, I will discuss a new, formal, measurement-driven and model-based automated technique, for the quantitative verification of systems with partly unknown dynamics. I will formulate this setup as a data-driven Bayesian inference problem, formally embedded within a quantitative, model-based verification procedure. I argue that the approach can be applied to complex physical systems (e.g., with spatially continuous variables), driven by external inputs and accessed under noisy measurements.
In the later part of the talk, I will concentrate on learning actions in a model, whilst verifying logical constraints, such as safety requirements. I will introduce a new paradigm called ‘Logically Constrained Reinforcement Learning’ to attain this, and explain its virtues and its application over complex systems.
The workshop was held on January 11th and 12th.
Logic has proved in the last decades a powerful tool in understanding complex systems. It is instrumental in the development of formal methods, which are mathematically based techniques obsessing on hard guarantees. Learning is a pervasive paradigm which has seen tremendous success recently. The use of statistical approaches yields practical solutions to problems which yesterday seemed out of reach. These two mindsets should not be kept apart, and many efforts have been made recently to combine the formal reasoning offered by logic and the power of learning.
The goal of this workshop is to bring together expertise from various areas to try and understand the opportunities offered by combining logic and learning.
There are 12 invited speakers and a light programme (less than 5h per day) so as to give enough time for discussions.
Add comment