SBMF 2025: 28TH BRAZILIAN SYMPOSIUM ON FORMAL METHODS
PROGRAM FOR FRIDAY, DECEMBER 5TH
Days:
previous day
all days

View: session overviewtalk overview

09:00-10:30 Session 15: Keynote 3
09:00
Formal Reasoning for Assuring Product Lines of Complex Systems
10:30-11:00Coffee Break
11:00-12:30 Session 16: AI, Availability and Contracts
11:00
Inference of Deterministic Finite Automata via Q-Learning

ABSTRACT. Traditional approaches to DFA inference stem from symbolic AI, including both active learning methods (e.g., Angluin’s L* algorithm and its variants) and passive techniques (e.g., Biermann and Feldman’s method, RPNI). Meanwhile, sub-symbolic AI, particularly machine learning, offers alternative paradigms for learning from data, such as supervised, unsupervised, and reinforcement learning (RL). In this paper, we investigate the use of Q-learning, a well-known reinforcement learning algorithm, for the passive inference of deterministic finite automata. Our core insight is that the learned Q-function, which maps state-action pairs to rewards, can be reinterpreted as the transition function of a DFA over a finite domain. This provides a novel bridge between sub-symbolic learning and symbolic representations. We demonstrate how Q-learning can be adapted for automaton inference and provide an evaluation on several examples.

11:30
Availability Model and Evaluation of Bus Rapid Transit Surveillance System

ABSTRACT. The integration of Information and Communication Technologies (ICT) has become essential to enhancing urban infrastructure and addressing challenges in modern cities, particularly in urban mobility. Bus Rapid Transit (BRT) systems are crucial for enhancing mobility, but they require robust monitoring to ensure safety and service quality, particularly at high-traffic stations. This paper presents a hierarchical availability model for monitoring systems in BRT stations, combining Reliability Block Diagrams (RBDs) to represent the system structure and Continuous-Time Markov Chains (CTMCs) to model the dynamic behavior of Edge Computing components. The proposed approach supports the evaluation of system availability and informs decision-making in the design and planning of smart urban infrastructure. A case study demonstrates the model's applicability in a realistic IoT-enabled BRT environment, highlighting its effectiveness in estimating availability metrics and improving service resilience. Evaluation results indicated a baseline system availability of 99.70%, translating to nearly 26 hours of annual downtime. Sensitivity analysis revealed the Edge computing unit as the most critical component, and implementing warm standby redundancy for this unit substantially improved system availability, reducing annual downtime by up to 76% in evaluated scenarios.

12:00
Resource Contracts for Active Objects

ABSTRACT. Workflows coordinate tasks across departments or organisations, where correct execution depends not only on control dependencies but also on the availability of shared resources. This paper presents ReAct, a resource-aware active object language for workflow modelling. In ReAct, method declarations serve as contracts: they specify alternative resource profiles in their signatures, giving methods multiple execution options when resources are limited. Methods can be invoked only once their dependency conditions are satisfied; at activation, a feasible resource profile is then selected and allocated. We encode the language in Maude and show how workflows can be executed, simulated, and verified against their declared dependencies and resource requirements.