Safety-critical decision-making often necessitates operating within complex and uncertain environments, typically characterized as partially-observable Multi-Agent Systems (MAS). Effective decision-making in these settings demands a profound understanding of the environment and accurate representation and quantification of epistemic uncertainty due to informational deficits. This uncertainty representation must reflect prior knowledge and dynamically integrate observational data. While Version Space Learning (VSL) offers a framework for set-based uncertainty representation, prior methods often depend on under-approximation of the actual version space, which falls short in safety-critical applications. We introduce a model checking-based VSL framework to enhance uncertainty representation and context-awareness in such applications. Our approach employs network of timed automata (NTA) to model the MAS environment, capturing its mechanisms and prior knowledge efficiently. The inherent non-determinism of timed automata facilitates an over-approximation of the actual version space, ensuring all plausible hypotheses are considered. We further refine the parameter ranges of the NTA using proof traces, optimizing the use of observational data. In a medical diagnosis case study, our framework identified a missing rule in a traditional rule-based system and provided interpretable and scalable results, demonstrating our method’s ability to improve decision-making accuracy and manage complex scenarios effectively.

The increasing demands for system complexity and robustness have prompted the integration of temporal logic into Multi-Agent Reinforcement Learning (MARL) to address tasks with non-Markovian properties. However, incorporating non-Markovian properties introduces additional computational complexities, as agents are required to integrate historical data into their decision-making process. Also, optimizing strategies within a multi-agent environment presents significant challenges due to the exponential growth of the state space with the number of agents. In this study, we introduce an innovative hierarchical MARL framework that synthesizes temporal equilibrium strategies through parity games and subsequently encodes them as individual reward machines for MARL coordination. More specifically, we reduce the strategy synthesis problem into an emptiness problem concerning parity games with optimized states and transitions. Following this synthesis step, the temporal equilibrium strategy is decomposed into individual reward machines for decentralized MARL. Theoretical proofs are provided to verify the consistency of the Nash equilibrium between the parallel composition of decomposed strategies and the original strategy. Empirical evidence confirms the efficacy of the proposed synthesis technique, showcasing its ability to reduce state space compared to the state-of-the-art tool. Furthermore, our study highlights the superior performance of the distributed MARL paradigm over centralized approaches when deploying decomposed strategies.

In the realm of 3D single object tracking (SOT), Siamese network-based algorithms have shown remarkable performance. However, they can lose track of targets in complex environments. To enhance tracking accuracy and continuity, in this paper we introduce a new re-detection mechanism with a dynamic anchor relocation strategy. This mechanism includes: (i) dynamic anchor generation: When tracking fails, dynamic anchors are generated and adjusted until the target is re-detected. The most confident anchor prediction becomes the tracking result; (ii) model aggregation: A re-detected module is integrated into the PTT-Net framework, significantly improving tracking accuracy compared to other algorithms; (iii) reliability assessment: An assessment criterion for tracking reliability in PTT-Net is established to balance accuracy and speed.

Reinforcement learning has been used to solve sequential decision-making problems in intelligent systems. However, current RL approaches suffer from slow convergence and reward sparsity, and its reward mechanism is challenging to deal with complex task specifications. As one of the software engineering practices, temporal logic can describe nonMarkovian task specifications, the synthesized strategy of which could be used as a priori knowledge to train the agents to interact with the environment efficiently. This paper considers the intelligent agent reacts to the environment with a high-level reactive temporal logic specification called Generalized Reactivity of rank 1 (GR(1)). We first use the synthesized strategy of GR(1) to construct the Markov Decision Process with a potentialbased reward machine, which integrates the environment with high-level reactive temporal specifications. Then we developed a topological-sort-based reward shaping approach to calculate the potential functions of the reward machine, based on which we used Q-learning to train the agents. Experiments on multitask learning show that the proposed approach outperforms the state-of-art algorithms in learning rate and optimal rewards. Also, compared with the value-iteration-based reward shaping approaches, our topological-sort-based reward shaping approach could handle the cases where the synthesized strategies are in the form of directed cyclic graphs.

Stepwise development supported by the Event-B formalism has been used in the domain of system design and verification. This refinement approach guarantees that safety properties are preserved, while additional reasoning is required to prove the preservation of liveness properties. Our previous work proposes to use real-time trigger-response properties to reason about liveness properties and timed properties in real-time systems. Conditions such as weak fairness assumptions, relative deadlock freedom, and conditional convergence are explored to eliminate Zeno behavior when modeling real-time systems. In this reasoning framework, some strong constraints do not apply to real-world cases. This paper extends our previous results by using strong fairness assumptions to relax these constraints. We present the proof obligations together with temporal properties to construct the theorems and proofs. Fairness assumptions are used to enforce real-time properties in Event-B models. The carrier-sense multiple access with collision detection protocol is used as a case study to illustrate the approach.

As the physical world evolves with time, safety-critical systems are usually used with time-dependent functionality. The design and implementation of real-time systems are challenging due to the complicated functional and timing requirements. Event - B formalization offers a stepwise development approach for specifying and verifying systems with mathematical techniques and tools. In this paper, we propose four realtime specification patterns, namely time response pattern, abort pattern, intermediate pattern and periodic pattern, to facilitate the specification of real-time properties in Event-B models. The proposed patterns are used in a dual-chamber pacemaker case study to specify and verify the timing cycles based on the requirements. The model is proved using the Rodin tool.

Abstraction and refinement offer a stepwise development approach to managing complexity in system design. Based on our previous work that extends Event-B models with high level real-time trigger-response properties, this paper presents refinement semantics of timed systems using behavioral traces. Forward simulation, which is a proof technique for refinement, is used to verify the consistency between different refinement levels. To prove refinement of trace semantics, we construct intermediate traces from concrete traces with a mapping function and prove the intermediate trace without stuttering events and states are abstract traces. Fairness assumptions, relative deadlock freedom, and conditional convergence are adopted in refinement steps to eliminate Zeno behavior in timed models. Based on the semantics, we develop refinement rules and strategies to perform refinement on timed models and refine real-time trigger-response properties into sequential or alternative sub-timing properties with proofs.

Event-B is a formal method for system-level modelling and analysis, which uses logic and set theory to describe discrete labelled transition systems. Timed transition systems have been introduced to incorporate timing constraints on transitions to describe real-time behaviours of the system. This paper proposes an approach to modelling high level timing constraints between different transitions with a timed trigger-response property. We present trace semantics for the trigger-response property and timed trigger-response property. This semantics provides a precise definition of valid trigger-response behaviours in Event-B machines. Based on the semantics, we develop proof obligations on Event-B machines under which all the traces of a machine satisfy the trigger-response property and the timed trigger-response property.