Bridging Social and Technical Compliance in Autonomous Systems through a Standardized Pattern Catalog

Research question

Autonomous systems are moving into places shared with people — roads, fields, residential areas. For them to be accepted, being safe and completing tasks on time is no longer enough: they also have to respect social norms, the implicit and context-dependent rules of acceptable conduct, such as yielding to a pedestrian or keeping quiet near homes in the evening. Timed and untimed Computation Tree Logic (TCTL and CTL), checked with tools such as UPPAAL on timed-automata models, are the standard way to verify technical properties. The paper asks how engineers can verify social norms in the same workflow, without hand-crafting error-prone temporal formulas that are hard to trace back to the original requirement.

Approach

The paper contributes a standardized catalog of reusable observer patterns covering both families of social norm distinguished in the literature:

• regulative norms, which constrain behaviour — permission, prohibition, obligation, exceptions (defeasible norms), role-based authority and graded compliance;
• constitutive norms, which create institutional facts, statuses and powers, following the “X counts as Y in context C” form.

Each pattern has a three-part interface: a natural-language template for requirements elicitation, a precise (T)CTL formalization, and an observer automaton that can be composed with an existing model. Each norm is monitored by a dedicated observer that does not change the system’s behaviour, so social properties can be co-verified alongside safety and liveness properties. The authors state that, to their knowledge, it is the first catalog to cover both norm families.

The running example is a fleet of autonomous tractors sharing peri-urban roads with workers, residents and traffic, with requirements such as not entering a residential zone after 5 pm unless carrying time-critical harvest, pulling over when vehicles queue behind, and entering a processing hub only with the clearance of an empowered human coordinator.

Results

The catalog is evaluated on seven UPPAAL models from smart-farming and autonomous-transport scenarios, addressing the reusability of the patterns, verification performance and scalability, the resolution of conflicts between norms, and the quantitative impact of social norms on behaviour, i.e. the trade-off between social compliance and performance.

Why it matters

The paper gives requirements and verification engineers a practical route from a stakeholder’s social expectation to a verified temporal property, and gives researchers in normative systems a bridge to established model-checking toolchains. It applies the specification-pattern idea, well known for technical timing and behavioural properties, to social and institutional requirements of autonomous systems.