English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In this paper, we investigate property verification problems inpartially-observed discrete-event systems (DES). Particularly, we areinterested in verifying observational properties that are related to theinformation-flow of the system. Observational properties considered hereinclude diagnosability, predictability, detectability and opacity, which havedrawn considerable attentions in the literature. However, in contrast toexisting results, where different verification procedures are developed fordifferent properties case-by-case, in this work, we provide a unified frameworkfor verifying all these properties by reducing each of them as an instance ofHyperLTL model checking. Our approach is based on the construction of a Kripkestructure that effectively captures the issue of unobservability as well as thefinite string semantics in partially-observed DES so that HyperLTL modelchecking techniques can be suitably applied. Then for each observationalproperty considered, we explicitly provide the HyperLTL formula to be checkedover the Kripke structure for the purpose of verification. Our approach isuniform in the sense that all different properties can be verified with thesame model checking engine. Furthermore, our unified framework also brings newinsights for classifying observational properties for partially-observed DES interms of their verification complexity.

A Unified Framework for Verification of Observational Properties for Partially-Observed Discrete-Event Systems