{"id":{"repo_id":"trento","oai_identifier":"oai:iris.unitn.it:11572/368759"},"canonical_url":"https://search.dev.ndltd.org/etd/trento/oai:iris.unitn.it:11572/368759","repository":{"repo_id":"trento","name":"Università degli Studi di Trento","base_url":"https://iris.unitn.it/oai/request"},"display":{"title":"A Formal Foundation of FDI Design via Temporal Epistemic Logic","abstract":"Autonomous systems must be able to detect and promptly react to faults. Fault Detection and Identification components (FDI) are in charge of detecting the occurrence of faults. The FDI depends on the concrete design of the system, needs to take into account how faults might interact, and can only have a partial view of the run-time state through sensors. For these reasons, the development of the FDI and certification of its correctness and quality are difficult tasks. This difficulty is compounded by the fact that current approaches for verification of the FDI rely on manual inspection and testing. Motivated by industrial case-studies from the European Space Agency, this thesis proposes a formal foundation for FDI design that covers specification, validation, verification, and synthesis. The Alarm Specification Language (ASLk) is introduced in order to formally capture a set of interesting and desirable properties of the FDI components. ASLk is equipped with a semantics based on Temporal Epistemic Logic, thus enabling reasoning about partially observable systems. Automated reasoning techniques can then be applied to perform validation, verification, and synthesis of the FDI. This formal process guarantees that the generated FDI satisfies the designer expectations. The problems deriving from this process were out of reach for existing model-checking techniques. Therefore, we develop novel and efficient techniques for model-checking temporal epistemic logic over infinite state systems.","abstract_html":"Autonomous systems must be able to detect and promptly react to faults. Fault Detection and Identification components (FDI) are in charge of detecting the occurrence of faults. The FDI depends on the concrete design of the system, needs to take into account how faults might interact, and can only have a partial view of the run-time state through sensors. For these reasons, the development of the FDI and certification of its correctness and quality are difficult tasks. This difficulty is compounded by the fact that current approaches for verification of the FDI rely on manual inspection and testing. Motivated by industrial case-studies from the European Space Agency, this thesis proposes a formal foundation for FDI design that covers specification, validation, verification, and synthesis. The Alarm Specification Language (ASLk) is introduced in order to formally capture a set of interesting and desirable properties of the FDI components. ASLk is equipped with a semantics based on Temporal Epistemic Logic, thus enabling reasoning about partially observable systems. Automated reasoning techniques can then be applied to perform validation, verification, and synthesis of the FDI. This formal process guarantees that the generated FDI satisfies the designer expectations. The problems deriving from this process were out of reach for existing model-checking techniques. Therefore, we develop novel and efficient techniques for model-checking temporal epistemic logic over infinite state systems.","abstract_has_math":false,"creators":["Gario, Marco"],"institution":"Università degli studi di Trento","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Cimatti, Alessandro"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2016,"date_issued":"2016","date_published":"2016","updated_at":"2026-07-24T05:04:17Z","subjects":["Settore INF/01 - Informatica","Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni","Settore MAT/01 - Logica Matematica"],"languages":["eng"],"rights":["info:eu-repo/semantics/closedAccess","license:Tutti i diritti riservati (All rights reserved)"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["http://dx.doi.org/10.15168/11572_368759","10.15168/11572_368759"],"render_values":[{"text":"http://dx.doi.org/10.15168/11572_368759","href":"http://dx.doi.org/10.15168/11572_368759","code":true},{"text":"10.15168/11572_368759","href":"https://doi.org/10.15168/11572_368759","code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/11572/368759","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Gario, Marco","Cimatti, Alessandro"]},{"key":"dc:creator","label":"Author","values":["Gario, Marco"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2016"]},{"key":"dc:publisher","label":"Institution","values":["Università degli studi di Trento","place:TRENTO"]},{"key":"dc:relation","label":"Dc Relation","values":["firstpage:1","lastpage:263","numberofpages:263"]},{"key":"dc:type","label":"Dc Type","values":["info:eu-repo/semantics/doctoralThesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Settore INF/01 - Informatica","Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni","Settore MAT/01 - Logica Matematica"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["info:eu-repo/semantics/closedAccess","license:Tutti i diritti riservati (All rights reserved)"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/11572/368759","http://dx.doi.org/10.15168/11572_368759","10.15168/11572_368759"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Autonomous systems must be able to detect and promptly react to faults. Fault Detection and Identification components (FDI) are in charge of detecting the occurrence of faults. The FDI depends on the concrete design of the system, needs to take into account how faults might interact, and can only have a partial view of the run-time state through sensors. For these reasons, the development of the FDI and certification of its correctness and quality are difficult tasks. This difficulty is compounded by the fact that current approaches for verification of the FDI rely on manual inspection and testing. Motivated by industrial case-studies from the European Space Agency, this thesis proposes a formal foundation for FDI design that covers specification, validation, verification, and synthesis. The Alarm Specification Language (ASLk) is introduced in order to formally capture a set of interesting and desirable properties of the FDI components. ASLk is equipped with a semantics based on Temporal Epistemic Logic, thus enabling reasoning about partially observable systems. Automated reasoning techniques can then be applied to perform validation, verification, and synthesis of the FDI. This formal process guarantees that the generated FDI satisfies the designer expectations. The problems deriving from this process were out of reach for existing model-checking techniques. Therefore, we develop novel and efficient techniques for model-checking temporal epistemic logic over infinite state systems."]},{"key":"dc:title","label":"Title","values":["A Formal Foundation of FDI Design via Temporal Epistemic Logic"]}]}],"canonical_facts":{"dc:contributor":["Gario, Marco","Cimatti, Alessandro"],"dc:creator":["Gario, Marco"],"dc:date":["2016"],"dc:description":["Autonomous systems must be able to detect and promptly react to faults. Fault Detection and Identification components (FDI) are in charge of detecting the occurrence of faults. The FDI depends on the concrete design of the system, needs to take into account how faults might interact, and can only have a partial view of the run-time state through sensors. For these reasons, the development of the FDI and certification of its correctness and quality are difficult tasks. This difficulty is compounded by the fact that current approaches for verification of the FDI rely on manual inspection and testing. Motivated by industrial case-studies from the European Space Agency, this thesis proposes a formal foundation for FDI design that covers specification, validation, verification, and synthesis. The Alarm Specification Language (ASLk) is introduced in order to formally capture a set of interesting and desirable properties of the FDI components. ASLk is equipped with a semantics based on Temporal Epistemic Logic, thus enabling reasoning about partially observable systems. Automated reasoning techniques can then be applied to perform validation, verification, and synthesis of the FDI. This formal process guarantees that the generated FDI satisfies the designer expectations. The problems deriving from this process were out of reach for existing model-checking techniques. Therefore, we develop novel and efficient techniques for model-checking temporal epistemic logic over infinite state systems."],"dc:identifier":["https://hdl.handle.net/11572/368759","http://dx.doi.org/10.15168/11572_368759","10.15168/11572_368759"],"dc:language":["eng"],"dc:publisher":["Università degli studi di Trento","place:TRENTO"],"dc:relation":["firstpage:1","lastpage:263","numberofpages:263"],"dc:rights":["info:eu-repo/semantics/closedAccess","license:Tutti i diritti riservati (All rights reserved)"],"dc:subject":["Settore INF/01 - Informatica","Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni","Settore MAT/01 - Logica Matematica"],"dc:title":["A Formal Foundation of FDI Design via Temporal Epistemic Logic"],"dc:type":["info:eu-repo/semantics/doctoralThesis"]},"updated_at":"2026-07-24T05:04:17Z"}