Control under Partial Observation w.r.t Rabin Specifications

This section addresses functions for supervisory controller synthesis under partial observation with Rabin specification. The synthesis approach combines control pattern expansion, epsilon observation, and pseudo-determinization to compute deterministic supervisors that enforce the specifications while respecting controllability and observability constraints. This approach was proposed by Thistle/Lamouchi in [W5].


Copyright (C) 2025 Changming Yang.

Partial Observation Control Problem

In the partial observation setting, the supervisor can only observe a subset of events Sigma_o ⊆ Sigma and control a subset of events Sigma_c ⊆ Sigma. The synthesis problem is to find a supervisor that:

  • Enforces the given specification

  • Respects controllability constraints (cannot disable uncontrollable events)

  • Respects observability constraints (decisions based only on observable events)

  • Maintains the Rabin acceptance condition

Synthesis Algorithm

The synthesis algorithm consists of the following steps:

  1. Product Construction: Compute the synchronous product of plant and specification
  2. Control Pattern Expansion: Expand the alphabet to include control patterns
  3. Epsilon Observation: Replace unobservable events with epsilon transitions
  4. Pseudo-Determinization: Convert to a deterministic Rabin automaton
  5. Trimming: Remove unreachable states

RabinCtrlPartialObs

Rabin control synthesis under partial observation with control patterns.

Signature:

RabinCtrlPartialObs(+In+ System GPlant, +In+ RabinAutomaton GSpec, +Out+ RabinAutomaton GSupervisor)

RabinCtrlPartialObs(+In+ RabinAutomaton GPlant, +In+ EventSet AContr, +In+ EventSet AObs, +In+ RabinAutomaton GSpec, +Out+ RabinAutomaton GSupervisor)

Detailed description:

This function performs complete supervisory control synthesis for Rabin automata under partial observation. It automatically extracts controllable and observable events from System attributes or accepts explicit event sets.

Algorithm

The function internally calls RabinProduct, ExpandToControlPatterns, EpsObservation, and PseudoDet in sequence to compute the supervisor.

Example

// 
System plant;
RabinAutomaton spec, supervisor;

// Set up plant with controllable and observable events
EventSet controllable;
controllable.Insert("a");
plant.SetControllable(controllable);

EventSet observable;  
observable.Insert("a");
observable.Insert("c");
plant.SetObservable(observable);

// Read specification
spec.Read("specification.gen");

// Synthesize supervisor
RabinCtrlPartialObs(plant, spec, supervisor);

// Write result
supervisor.Write("supervisor.gen");

RabinProduct

Detailed description:

Computes the synchronous product (parallel composition) of two Rabin automata. The result combines the behaviors of both automata with a properly composed Rabin acceptance condition.

Example

RabinAutomaton plant, spec, product;

plant.Read("plant.gen");
spec.Read("specification.gen");

RabinProduct(plant, spec, product);
product.Write("product.gen");

EpsObservation

Epsilon observation for Rabin automata by replacing unobservable events with epsilon events.

Signature:

EpsObservation(+In+ RabinAutomaton G, +Out+ RabinAutomaton GRes)

Detailed description:

Performs epsilon observation on a Rabin automaton by replacing unobservable events with epsilon transitions. This transformation preserves the acceptance condition while enabling the handling of partial observability.

Algorithm

The function identifies unobservable events and creates epsilon transitions that maintain the control pattern structure necessary for synthesis.

PseudoDet

Pseudo-determinization algorithm for Rabin automata.

Signature:

PseudoDet(+In+ RabinAutomaton G, +Out+ RabinAutomaton GRes)

Detailed description:

Converts a nondeterministic Rabin automaton to an equivalent deterministic Rabin automaton using the pseudo-determinization algorithm. The algorithm uses labeled trees to track acceptance condition during determinization.

Algorithm

The pseudo-determinization algorithm maintains tree structures for each state to track which original states are reachable and their acceptance status. This ensures the Rabin acceptance condition is preserved.

Example

RabinAutomaton nondet, det;

nondet.Read("nondeterministic.gen");
PseudoDet(nondet, det);
det.Write("deterministic.gen");

Complete Synthesis Example

The following example demonstrates the complete synthesis process: 

// Set up plant model
System plant;
Generator machine1, machine2;
machine1.Read("machine1.gen");  
machine2.Read("machine2.gen");
Parallel(machine1, machine2, plant);

// Configure controllability
EventSet controllable;
controllable.Insert("start");
plant.SetControllable(controllable);

// Configure observability  
EventSet observable;
observable.Insert("start");
observable.Insert("done");
plant.SetObservable(observable);

// Read specification
RabinAutomaton spec;
spec.Read("specification.gen");

// Synthesize supervisor (one-line solution!)
RabinAutomaton supervisor;
RabinCtrlPartialObs(plant, spec, supervisor);

// Verify and save result
if(supervisor.Empty()) {
  std::cout << "No supervisor exists!" <<  std::endl;
} else {
  std::cout << "Supervisor generated successfully" <<  std::endl;
  supervisor.Write("supervisor.gen");
}

libFAUDES 2.33l --- 2025.09.16 --- with "omegaaut-synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-priorities-luabindings-hybrid-example-pybindings"

>>