#### Model checking dynamic legal specifications

Software is increasingly influential in many aspects of our daily lives as social systems and software systems are increasingly intertwined in the, for example, healthcare, governmental, and mobility domains. Especially in distributed settings, the behaviour of software is ideally directly subjected to laws, regulations, contracts and (organisational) policies. To this end, software languages are being designed to formalise such social policies in attempts to automate compliance such as smart contracts and legal specification languages. However, a challenge to the application of such languages is that social policies are subjected to constant change. For example, governments, and the EU in particular, are issueing laws and regulations that affect software at a rapid pace. Moreover, legal experts may modify their interpretations of laws and regulations and their embedding in organisational policies. How can a system that automates compliance based on formal interpretations of social policies be updated dynamically? And how can we ensure such updates do not introduce inconsistencies or break certain invariants?

The goal of this project is to investigate in particular the second question. A partial answer is given by earlier work on the design and implementation of eFLINT, a domain-specific language (DSL) developed to reason about (legal) scenarios and to automate compliance of software systems [1,2]. The language enables the specification of properties based on LTL formulae known from model checking formalisms [3,4]. With the property language of eFLINT, safety and liveness properties can be expressed to analyse sets of scenarios and to automatically find counter-examples: scenarios that violate a given property. In this project you will contribute by developing a methodology to use such properties to gain confidence in dynamic updates to social policies. This can be achieved, for example, by automatically checking properties after every update to the policy, akin to self-testing in continuous integration. 

This project is to be executed in three steps. Firstly, a conceptual solution (algorithms, language extensions) is to be designed based on the current design of eFLINT and its existing property language. Secondly, the feasibility of the solution is to be investigated by testing an implementation against realistic example scenarios of your choosing. Thirdly, optimisations are to be investigated and implemented that increase the practicality of the approach. As such, this is a highly ambitious project that combines theory and practice in the domains of language design, compiler construction, model checking and software evolution. 

[1] Van Binsbergen, L. Thomas, et al. eFLINT: a domain-specific language for executable norm specifications. DOI: https://doi.org/10.1145/3425898.3426958
[2] Van Binsbergen, L. Thomas, et al. Dynamic generation of access control policies from social policies. DOI: https://doi.org/10.1016/j.procs.2021.12.221
[3] R. Cavada et al. The nuXmv Symbolic Model Checker, in Computer Aided Verification. DOI: https://doi.org/10.1007/978-3-319-08867-9_22
[4] Clarke, E.M., Henzinger, T.A., Veith, H. Introduction to Model Checking. In: Handbook of Model Checking. DOI: https://doi.org/10.1007/978-3-319-10575-8_1