This thesis is to be carried out in cooperation with Gerardo Schneider from the University of Gothenburg.
Motivation and Importance
Normative systems—systems governed by rules such as obligations, permissions, and prohibitions—are central to many modern domains, including autonomous systems, multi-agent coordination, legal-tech, and business process compliance. As software increasingly operates in open, dynamic environments, ensuring that behavior adheres to specified norms becomes critical. Violations can lead not only to system failures but also to legal, ethical, or financial consequences. Runtime monitoring provides a practical solution by observing executions and detecting (or anticipating) deviations from prescribed norms.
Background: C-O Diagrams
C-O Diagrams (Contract-Oriented Diagrams), introduced by Gerardo Schneider and collaborators, are a visual formalism for specifying normative systems. They provide a structured way to represent:
- Obligations (O): actions that must be performed,
- Prohibitions (F): actions that must not be performed,
- Permissions (P): actions that are allowed,
along with timing constraints, reparations (what should happen if a norm is violated), and hierarchical compositions of norms.
These diagrams combine an intuitive graphical notation with a formal semantics, making them suitable for both human understanding and automated analysis. Their semantics can typically be mapped to formal models such as timed automata or transition systems.
Research Objective
The goal of this thesis is to develop a method for automatically synthesizing runtime monitors from C-O Diagrams. These monitors should observe execution traces and determine compliance or violations of the specified norms, ideally in real time.
Key Tasks and Methodology
- Formalization of Semantics
- Precisely define (or adopt existing) formal semantics for C-O Diagrams.
- Ensure that obligations, prohibitions, permissions, timing constraints, and reparations are unambiguously captured.
- Mapping to Monitorable Models
- Translate C-O Diagrams into an intermediate formal representation suitable for monitoring, such as finite-state machines, timed automata, or stream-based formalisms.
- Address how to encode deadlines, conditional norms, and reparations.
- Monitor Synthesis
- Design algorithms that generate executable monitors from the formal representation.
- Ensure that monitors can:
- Detect violations and satisfactions of norms,
- Handle partial observability (if relevant),
- Manage temporal constraints efficiently.
- Correctness and Properties
- Prove that the synthesized monitors are sound (no false positives) and complete (no missed violations) with respect to the formal semantics.
- Analyze properties such as determinism, minimality, and runtime efficiency of the monitors.
- Implementation and Evaluation
- Develop a prototype tool that takes C-O Diagrams as input and produces monitors.
- Evaluate on case studies (e.g., service-level agreements, autonomous agent protocols).
- Compare with existing monitoring approaches if applicable.
- Extensions (Optional)
- Support for probabilistic or uncertain environments,
- Integration with enforcement mechanisms (not just detection),
- User-friendly feedback or visualization of violations.
Expected Contributions
- A systematic approach for translating C-O Diagrams into runtime monitors,
- Formal guarantees about the correctness of the monitors,
- A prototype implementation and evaluation demonstrating applicability in realistic scenarios.
This thesis connects high-level normative specifications with runtime verification techniques, contributing to the development of more reliable and trustworthy rule-governed systems.
Literature
- Camilleri, J. J., Paganelli, G., Schneider, G. A CNL for Contract-Oriented Diagrams. (CNL 2014)
- Díaz, G., Cambronero, M. E., Martínez, E., Schneider, G. Specification and Verification of Normative Texts using C-O Diagrams. (IEEE TSE, 2014)