arXiv subjects

Tiago Ferreira

Publications and source records attributed to Tiago Ferreira.

12 recordsLinked to original sources

arXiv2026

Weighted NetKAT: A Programming Language For Quantitative Network Verification

We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative network properties. The language is parametric on a semiring, enabling the treatment of a wide range of quantities in a uniform way. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata (WNKA) capturing the stateful behavior of our language. With WNKA, we obtain a class of generic decision procedures for reasoning about quantitative safety and reachability in a fully automatic way, even in the presence of possibly unbounded iteration. We demonstrate the applicability of our framework in a case study using Internet2's Abilene network as the underlying topology.

cs.PL↗

arXiv2026

A Fast Quantitative Analyzer for NetKAT

When designing a network, engineers must navigate trade-offs (e.g., one topology offers more aggregate bandwidth, another lower latency or better resilience) that demand reasoning about quantitative properties. We present a fast analyzer for quantitative network properties based on weighted NetKAT (wNetKAT), a domain-specific language that provides a semantic foundation for quantitative reasoning by modeling network behavior using weights drawn from a semiring. At the core of our development is the design of a symbolic data structure -- weighted symbolic packet programs (wSPPs) -- that compactly represent the semantics of weighted policies, for which a direct implementation would be intractable. We show how to compute all policy constructs symbolically; unsurprisingly, the crux is Kleene star, for which we design a tailored algorithm. We further develop trace-carrying Pareto semirings, which compute multi-objective frontiers together with the network paths that realize them. We formalize the development in Lean and provide an optimized Rust implementation. Being parametric on a semiring, our implementation covers both classical and quantitative analyses: we show that it is competitive with KATch, a heavily optimized Boolean-reachability verifier, and orders of magnitude faster than McNetKAT and Storm on probabilistic analyses. A case study comparing Fat-tree and Jellyfish data-center topologies shows the framework supports multi-objective design-time analysis.

cs.PL↗

arXiv2026

Photonic Extreme Learning Machines using Event-Based detection

Photonic extreme learning machines use random optical propagation, detection nonlinearity, and a trained linear readout for energy-efficient and scalable optical computing. However, conventional intensity readout with CCD or CMOS cameras constrain the dimensionality of the hidden representation space. Here, we experimentally replace intensity detection with event-based camera, whose thresholded log-intensity response provides alternative pixel-wise hidden representations: first-event time, binary activation, and event count. In nonlinear two spiral classification task we obtain accuracies of $93\pm 3\%$ with strong intrinsic generalization, and comparable ridge and pseudo-inverse performance indicating sample-limited effective dimensionality. Regression results reveal sensitivity to systematic optical-intensity drift, identifying stability requirements for future event-based PELMs. These results establish event-based detection as a route toward richer photonic hidden representations while clarifying current limitations.

physics.optics↗

arXiv2026

SMT-Based Active Learning of Weighted Automata

We present an SMT-based active learning algorithm for nondeterministic weighted automata (WFAs) as a practical and robust alternative to Hankel/L*-style methods. Our algorithm is parametric in a given semiring and, if it terminates, guaranteed to produce minimal WFAs. We prove partial correctness and provide a sufficient termination condition, which in particular implies termination for all finite semirings. Our extensive experimental evaluation shows that our algorithm is capable of learning numerous minimal WFAs over both finite and infinite semirings, vastly outperforms a naive baseline, and is competitive with a state-of-the-art algorithm while producing significantly smaller automata and requiring less interaction with the teacher.

cs.FL↗

arXiv2025

Multimodal Speckle-polarization Fiber-optic Sensing for Localized and High-bandwidth Vibration Monitoring

High-bandwidth and multi-point acoustic and vibration sensing is a critical asset for real-time condition monitoring, maintenance, and surveillance applications. In the case of large scales and harsh environments, optical fiber distributed sensing has emerged as a compelling alternative to electronic transducers, featuring lower installation and maintenance costs, along with compact footprints and enhanced robustness. Yet, current distributed fiber-optic sensing solutions are typically costly and face a resolution-bandwidth tradeoff. In this work, we present an alternative fiber-optic vibration sensing strategy that harnesses a multimodal architecture combining speckle and polarization interrogation. The experimental results demonstrate the concept by achieving speckle-based signal source localization with centimeter-range spatial resolution, while obtaining a high-fidelity waveform reconstruction over at least 100 Hz-40 kHz bandwidth via the polarimetric sensing part. Overall, the work establishes a general and promising blueprint to harness multimodality in fiber sensing and break single-modality constraints.

physics.optics↗

arXiv2025

RFSeek and Ye Shall Find

Requests for Comments (RFCs) are extensive specification documents for network protocols, but their prose-based format and their considerable length often impede precise operational understanding. We present RFSeek, an interactive tool that automatically extracts visual summaries of protocol logic from RFCs. RFSeek leverages large language models (LLMs) to generate provenance-linked, explorable diagrams, surfacing both official state machines and additional logic found only in the RFC text. Compared to existing RFC visualizations, RFSeek's visual summaries are more transparent and easier to audit against their textual source. We showcase the tool's potential through a series of use cases, including guided knowledge extraction and semantic diffing, applied to protocols such as TCP, QUIC, PPTP, and DCCP. In practice, RFSeek not only reconstructs the RFC diagrams included in some specifications, but, more interestingly, also uncovers important logic such as nodes or edges described in the text but missing from those diagrams. RFSeek further derives new visualization diagrams for complex RFCs, with QUIC as a representative case. Our approach, which we term \emph{Summary Visualization}, highlights a promising direction: combining LLMs with formal, user-customized visualizations to enhance protocol comprehension and support robust implementations.

cs.NI↗

arXiv2025

Active Learning of Symbolic NetKAT Automata

NetKAT is a domain-specific programming language and logic that has been successfully used to specify and verify the behavior of packet-switched networks. This paper develops techniques for automatically learning NetKAT models of unknown networks using active learning. Prior work has explored active learning for a wide range of automata (e.g., deterministic, register, Büchi, timed etc.) and also developed applications, such as validating implementations of network protocols. We present algorithms for learning different types of NetKAT automata, including symbolic automata proposed in recent work. We prove the soundness of these algorithms, build a prototype implementation, and evaluate it on a standard benchmark. Our results highlight the applicability of symbolic NetKAT learning for realistic network configurations and topologies.

cs.PL↗

arXiv2023

Conflict-Aware Active Automata Learning

Active automata learning algorithms cannot easily handle conflict in the observation data (different outputs observed for the same inputs). This inherent inability to recover after a conflict impairs their effective applicability in scenarios where noise is present or the system under learning is mutating. We propose the Conflict-Aware Active Automata Learning (C3AL) framework to enable handling conflicting information during the learning process. The core idea is to consider the so-called observation tree as a first-class citizen in the learning process. Though this idea is explored in recent work, we take it to its full effect by enabling its use with any existing learner and minimizing the number of tests performed on the system under learning, specially in the face of conflicts. We evaluate C3AL in a large set of benchmarks, covering over 30 different realistic targets, and over 18,000 different scenarios. The results of the evaluation show that C3AL is a suitable alternative framework for closed-box learning that can better handle noise and mutations.

cs.FL↗

arXiv2023

Conflict-Aware Active Automata Learning (Extended Version)

cs.LG↗

arXiv2022

Tree-Based Adaptive Model Learning

We extend the Kearns-Vazirani learning algorithm to be able to handle systems that change over time. We present a new learning algorithm that can reuse and update previously learned behavior, implement it in the LearnLib library, and evaluate it on large examples, to which we make small adjustments between two runs of the algorithm. In these experiments our algorithm significantly outperforms both the classic Kearns-Vazirani learning algorithm and the current state-of-the-art adaptive algorithm.

cs.FL↗

arXiv2021

Prognosis: Closed-Box Analysis of Network Protocol Implementations

We present Prognosis, a framework offering automated closed-box learning and analysis of models of network protocol implementations. Prognosis can learn models that vary in abstraction level from simple deterministic automata to models containing data operations, such as register updates, and can be used to unlock a variety of analysis techniques -- model checking temporal properties, computing differences between models of two implementations of the same protocol, or improving testing via model-based test generation. Prognosis is modular and easily adaptable to different protocols (e.g., TCP and QUIC) and their implementations. We use Prognosis to learn models of (parts of) three QUIC implementations -- Quiche (Cloudflare), Google QUIC, and Facebook mvfst -- and use these models to analyze the differences between the various implementations. Our analysis provides insights into different design choices and uncovers potential bugs. Concretely, we have found critical bugs in multiple QUIC implementations, which have been acknowledged by the developers.

cs.NI↗

arXiv2019

Symbolic Register Automata

Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite alphabets, respectively. Both automata models have interesting applications and have been successful in their own right. In this paper, we introduce Symbolic Register Automata, a new model that combines features from both symbolic and register automata, with a view on applications that were previously out of reach. We study their properties and provide algorithms for emptiness, inclusion and equivalence checking, together with experimental results.

cs.FL↗