Searcharxiv⌕ Search

arXiv subjects

Georgiana Caltais

Publications and source records attributed to Georgiana Caltais.

At least 19 recordsLinked to original sources
arXiv2026

Actual causality in fault trees

Fault trees are a widely used as effective risk models for complex systems, answering the question "what can go wrong?", especially through minimal cut set analysis. We study fault trees from the perspective of Halpern & Pearl's theory of actual causality. This allows us to use fault trees to answer the question "why has it gone wrong?", which is fundamental to failure diagnostics. We give a complete classification of each of the different notions of actual causality in terms of the fault tree's graph structure and logical structure, and show how minimal cut sets give rise to actual causes.

cs.AI↗
arXiv2026

Ontology-Grounded Capability Interaction Graphs: From Knowledge Graphs to Fault Trees

The development of Cyber-Physical Systems (CPSs) is inherently multidisciplinary, involving expertise from domains such as software engineering, electrical engineering, and mechatronics. throughout the lifecycle of the system, from design to deployment. Ensuring system reliability in Cyber-Physical Systems (CPSs) requires the identification and analysis of potential failures and their cascading effects. However, reliability modeling remains a challenging and error-prone activity, as it often depends on tacit expert knowledge, incomplete documentation of failure modes, and limited consideration of interactions between subsystems. To address these challenges, this paper introduce the Capability Interaction Graph (CIG), an ontology-driven representation of CPS architectures grounded in the Unified Foundational Ontology (UFO). Due to its graph-based structure, a CIG is naturally represented as a knowledge graph (KG), enabling the explicit capture of functional dependencies and system semantics. Building upon this representation, we propose an automated synthesis algorithm for generating Fault Trees (FTs) directly from CIGs encoded as knowledge graphs. Fault Tree Analysis provides an effective mechanism for evaluating critical failure properties, including failure propagation paths and minimal cut set sets. Our approach reduces this complexity by leveraging CIGs and knowledge graphs. We provide a common semantic representation across engineering domains and support the automated generation of reliability models.

cs.SE↗
arXiv2026

Circular Induction

The Circularity Principle was successfully applied for developing a coinductive proving technique, known as circular coinduction. In this paper, we show that the same principle can be used to develop an inductive proving technique. A main advantage of this uniform approach is that the two proving techniques can be easily combined during the verification process. Circular induction is simple, flexible, generic, and therefore it is a good candidate framework for combining different proving schemes into a competitive tool. We exhibit this potential by presenting how the circular induction is implemented in CIRC, a prover built around the Circularity Principle. Disclaimer. This paper was written in 2010, at the time the CIRC prover was developed, and the main body reflects the state of the work and of the prover as of that date. For this arXiv technical report, only the related-work discussion (Section 6) and the concluding section have been revised: Section 6 has been extended to situate circular induction within the cyclic-proof and infinite-descent literature that has appeared or matured since 2010. No other part of the paper-its definitions, results, proofs, examples, or implementation description-has been modified, and the technical content should be read as a 2010 contribution. References to developments after 2010 appear only in the updated related-work section.

cs.LO↗
arXiv2025

Fault Tree Synthesis from Knowledge Graphs

A truly effective diagnostic system provides system engineers with valuable insights into the behavior of their machines, leveraging a rich body of (often tacit) expertise. Much of this expertise typically resides in written documentation or troubleshooting manuals, which are frequently imprecise or vaguely specified. Therefore, methods for formalizing this knowledge, such as through the use of knowledge graphs, are of particular interest. However, ensuring that the extracted knowledge (ideally in a semi-automatic way) encapsulates sufficient semantic depth for system-level diagnostics is a challenging task. In this paper, we propose a minimal format for knowledge graphs that is semantically rich enough to facilitate the synthesis of meaningful fault trees. Fault trees offer an intuitive and efficient means for systematic failure analysis, enabling engineers to assess all potential failure modes in a structured, hierarchical manner. The methodology is applied to the Lycoming O-320 engine, showing that meaningful fault trees can be synthesized from only structural and functional knowledge of the system, defined by the proposed conceptual model.

cs.OH↗
arXiv2024

Proceedings Combined 31st International Workshop on Expressiveness in Concurrency and 21st Workshop on Structural Operational Semantics

This volume contains the proceedings of EXPRESS/SOS 2024: the Combined 31st International Workshop on Expressiveness in Concurrency and the 21st Workshop on Structural Operational Semantics, which was held in Calgary, Canada, as an affiliated workshop of CONFEST 2024. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models.

cs.FL↗
arXiv2024

Tracer: A Tool for Race Detection in Software Defined Network Models

Software Defined Networking (SDN) has become a new paradigm in computer networking, introducing a decoupled architecture that separates the network into the data plane and the control plane. The control plane acts as the centralized brain, managing configuration updates and network management tasks, while the data plane handles traffic based on the configurations provided by the control plane. Given its asynchronous distributed nature, SDN can experience data races due to message passing between the control and data planes. This paper presents Tracer, a tool designed to automatically detect and explain the occurrence of data races in DyNetKAT SDN models. DyNetKAT is a formal framework for modeling and analyzing SDN behaviors, with robust operational semantics and a complete axiomatization implemented in Maude. Built on NetKAT, a language leveraging Kleene Algebra with Tests to express data plane forwarding behavior, DyNetKAT extends these capabilities by adding primitives for communication between the control and data planes. Tracer exploits the DyNetKAT axiomatization and enables race detection in SDNs based on Lamport vector clocks. Tracer is a publicly available tool.

cs.FL↗
arXiv2023

Proceedings Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics

This volume contains the proceedings of EXPRESS/SOS 2023: the Combined 30th International Workshop on Expressiveness in Concurrency and the 20th Workshop on Structural Operational Semantics, which was held in Antwerp, Belgium, as an affiliated workshop of CONCUR 2023, the 34rd International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models.

cs.LO↗
arXiv2022

Counterfactual Causality in Networks

In this abstract we propose a framework for explaining violations of safety properties in Software Defined Networks, using counterfactual causal reasoning.

cs.FL↗
arXiv2021

DyNetKAT: An Algebra of Dynamic Networks

We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory to provide an efficient reasoning method about safety properties for dynamic networks. We implement our equational theory in DyNetiKAT -- a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our initial tool prototype.

cs.NI↗
arXiv2021

Explaining Safety Failures in NetKAT

This work introduces a concept of explanations with respect to the violation of safe behaviours within software defined networks (SDNs) expressible in NetKAT. The latter is a network programming language based on a well-studied mathematical structure, namely, Kleene Algebra with Tests (KAT). Amongst others, the mathematical foundation of NetKAT gave rise to a sound and complete equational theory. In our setting, a safe behaviour is characterised by a NetKAT policy, or program, which does not enable forwarding packets from an ingress i to an undesirable egress e. We show how explanations for safety violations can be derived in an equational fashion, according to a modification of the existing NetKAT axiomatisation. We propose an approach based on the Maude system for actually computing the undesired behaviours witnessing the forwarding of packets from i to e as above. SDN-SafeCheck is a tool based on Maude equational theories satisfying important properties such as Church-Rosser and termination. SDN-SafeCheck automatically identifies all the undesired behaviours leading to e, covering forwarding paths up to a user specified size.

cs.FL↗
arXiv2019

Explaining SDN Failures via Axiomatisations

This work introduces a concept of explanations with respect to the violation of safe behaviours within software defined networks (SDNs) expressible in NetKAT. The latter is a network programming language that is based on a well-studied mathematical structure, namely, Kleene Algebra with Tests (KAT). Amongst others, the mathematical foundation of NetKAT gave rise to a sound and complete equational theory. In our setting, a safe behaviour is characterised by a NetKAT policy which does not enable forwarding packets from ingress to an undesirable egress. Explanations for safety violations are derived in an equational fashion, based on a modification of the existing NetKAT axiomatisation.

cs.FL↗
arXiv2019

Causality for General LTL-definable Properties

In this paper we provide a notion of causality for the violation of general Linear Temporal Logic (LTL) properties. The current work is a natural extension of the previously proposed approach handling causality in the context of LTL-definable safety properties. The major difference is that now, counterexamples of general LTL properties are not merely finite traces, but infinite lasso-shaped traces. We analyze such infinite counterexamples and identify the relevant ordered occurrences of causal events, obtained by unfolding the looping part of the lasso shaped counterexample sufficiently many times. The focus is on LTL properties from practical considerations: the current results are to be implemented in QuantUM, a tool for causality checking, that exploits explicit state LTL model checking.

cs.FL↗
arXiv2016

(De-)Composing Causality in Labeled Transition Systems

In this paper we introduce a notion of counterfactual causality in the Halpern and Pearl sense that is compositional with respect to the interleaving of transition systems. The formal framework for reasoning on what caused the violation of a safety property is established in the context of labeled transition systems and Hennessy Milner logic. The compositionality results are devised for non-communicating systems.

cs.LO↗
arXiv2015

On the Verification of SCOOP Programs

In this paper we focus on the development of a toolbox for the verification of programs in the context of SCOOP -- an elegant concurrency model, recently formalized based on Rewriting Logic (RL) and Maude. SCOOP is implemented in Eiffel and its applicability is demonstrated also from a practical perspective, in the area of robotics programming. Our contribution consists in devising and integrating an alias analyzer and a Coffman deadlock detector under the roof of the same RL-based semantic framework of SCOOP. This enables using the Maude rewriting engine and its LTL model-checker "for free", in order to perform the analyses of interest. We discuss the limitations of our approach for model-checking deadlocks and provide solutions to the state explosion problem. The latter is mainly caused by the size of the SCOOP formalization which incorporates all the aspects of a real concurrency model. On the aliasing side, we propose an extension of a previously introduced alias calculus based on program expressions, to the setting of unbounded program executions such as infinite loops and recursive calls. Moreover, we devise a corresponding executable specification easily implementable on top of the SCOOP formalization. An important property of our extension is that, in non-concurrent settings, the corresponding alias expressions can be over-approximated in terms of a notion of regular expressions. This further enables us to derive an algorithm that always stops and provides a sound over-approximation of the "may aliasing" information, where soundness stands for the lack of false negatives.

cs.SE↗
arXiv2015

Coalgebraic Tools for Bisimilarity and Decorated Trace Semantics

The modelling, specification and study of the semantics of concurrent reactive systems have been interesting research topics for many years now. The aim of this thesis is to exploit the strengths of the (co)algebraic framework in modelling reactive systems and reasoning on several types of associated semantics, in a uniform fashion. In particular, we are interested in handling notions of behavioural equivalence/preorder ranging from bisimilarity for systems that can be represented as non-deterministic coalgebras, to decorated trace semantics for labelled transition systems and probabilistic systems, and testing semantics for labelled transition systems with internal behaviour. Moreover, we aim at deriving a suite of corresponding verification algorithms suitable for implementation in automated tools.

cs.LO↗
arXiv2014

Expression-based aliasing for OO-languages

Alias analysis has been an interesting research topic in verification and optimization of programs. The undecidability of determining whether two expressions in a program may reference to the same object is the main source of the challenges raised in alias analysis. In this paper we propose an extension of a previously introduced alias calculus based on program expressions, to the setting of unbounded program executions s.a. infinite loops and recursive calls. Moreover, we devise a corresponding executable specification in the K-framework. An important property of our extension is that, in a non-concurrent setting, the corresponding alias expressions can be over-approximated in terms of a notion of regular expressions. This further enables us to show that the associated K-machinery implements an algorithm that always stops and provides a sound over-approximation of the "may aliasing" information, where soundness stands for the lack of false negatives. As a case study, we analyze the integration and further applications of the alias calculus in SCOOP. The latter is an object-oriented programming model for concurrency, recently formalized in Maude; K-definitions can be compiled into Maude for execution.

cs.PL↗
arXiv2014

Coffman deadlocks in SCOOP

In this paper we address the deadlock detection problem in the context of SCOOP - an OO-programming model for concurrency, recently formalized in Maude. We present the integration of a deadlock detection mechanism on top of the aforementioned formalization and analyze how an abstract semantics of SCOOP based on a notion of "may alias expressions" can contribute to improving the deadlock detection procedure.

cs.PL↗