Opacity Verification and Fault Diagnosis in the Framework of Switching Output Automata
type: CreativeWork
description: Security and reliability in cyber-physical systems depend not only on which operational mode the system occupies, but also on how long it remains there. In practice, external observers see piecewise-constant output signals (power consumption levels, alarm indicators, aggregate measurements) together with their durations, rather than internal state transitions or continuous trajectories. Classical discrete-event models capture event sequences but lack native timing semantics, while dense-time formalisms such as timed automata face undecidability or prohibitive complexity for verification tasks involving both timing constraints and partial observability. This dissertation introduces the Switching Output Automaton (SOA) framework to address this gap. SOA models what observers see in practice: output symbols and their durations. The key innovation is a minimum dwell time constraint that requires any two consecutive events to be separated by at least a fixed positive duration. This constraint reflects physical reality and enables decidable verification by bounding the rate of observable changes. SOA combines continuous-time semantics with a set-valued output function that creates observational ambiguity independent of timing, allowing multiple states to share output symbols. We apply this framework to two timing-aware security and reliability problems. First, for opacity verification, we establish decidable procedures for both current-state opacity (where secrets are discrete states) and timed opacity (where secrets are global-state-duration triples specifying which combinations of discrete state, output, and dwell time must remain confidential). For timed opacity, verification proceeds by constructing a secret-dependent evolution automaton that applies fine-grained time discretization only to vulnerable global states, then building an observer automaton through subset construction, and finally reducing opacity to reachability analysis. This approach achieves decidabilit…
abstract: Security and reliability in cyber-physical systems depend not only on which operational mode the system occupies, but also on how long it remains there. In practice, external observers see piecewise-constant output signals (power consumption levels, alarm indicators, aggregate measurements) together with their durations, rather than internal state transitions or continuous trajectories. Classical discrete-event models capture event sequences but lack native timing semantics, while dense-time formalisms such as timed automata face undecidability or prohibitive complexity for verification tasks involving both timing constraints and partial observability. This dissertation introduces the Switching Output Automaton (SOA) framework to address this gap. SOA models what observers see in practice: output symbols and their durations. The key innovation is a minimum dwell time constraint that requires any two consecutive events to be separated by at least a fixed positive duration. This constraint reflects physical reality and enables decidable verification by bounding the rate of observable changes. SOA combines continuous-time semantics with a set-valued output function that creates observational ambiguity independent of timing, allowing multiple states to share output symbols. We apply this framework to two timing-aware security and reliability problems. First, for opacity verification, we establish decidable procedures for both current-state opacity (where secrets are discrete states) and timed opacity (where secrets are global-state-duration triples specifying which combinations of discrete state, output, and dwell time must remain confidential). For timed opacity, verification proceeds by constructing a secret-dependent evolution automaton that applies fine-grained time discretization only to vulnerable global states, then building an observer automaton through subset construction, and finally reducing opacity to reachability analysis. This approach achieves decidabilit…
author: LIU, TIANYU
language: eng
keywords: Settore ING-INF/04 - Automatica
date published: 2026-02-27T00:00:00+01:00
date modified: 2026-07-24T01:29:55Z
provider: Università di Cagliari
publisher: Networked Digital Library of Theses and Dissertations
type: WebPage
source organization: Università degli Studi di Cagliari

PropertyValue
property ID: Handle
value: https://hdl.handle.net/11584/475188