arXiv subjects

Joseph Sifakis

Publications and source records attributed to Joseph Sifakis.

At least 19 recordsLinked to original sources

arXiv2026

From Automated to Autonomous: Hierarchical Agent-native Network Architecture (HANA)

Realizing Level 4/5 Autonomous Networks (AN) demands a shift from static automation to agent-native intelligence. Current operations, reliant on rigid scripts, lack the cognitive agency to handle off-nominal conditions. To address this, this letter proposes a hierarchical multi-agent reference architecture enabling high-level autonomy. The framework features a Dual-Driven Orchestrator that coordinates specialized Executive Agents, supported by a shared Public Memory for unified domain knowledge. A key innovation is the integration of agent self-awareness, which empowers the system to harmonize deliberative strategic governance with reflexive fault recovery. We instantiate and validate this architecture within a 5G Core environment. Case studies demonstrate that the system sustains critical throughput under congestion and reduces Mean Time to Repair (MTTR) by 86%, confirming its efficacy in unifying strategic planning with operational resilience.

cs.AI↗

arXiv2026

Compositionally Safe Construction of Autonomous Driving Systems

Developing safe autonomous driving systems is a major scientific and technical challenge. Existing AI-based end-to-end solutions do not offer the necessary safety guarantees, while traditional systems engineering approaches are defeated by the complexity of the problem. We study a method for building compositionally safe autonomous driving systems, based on the assumption that the capability to drive boils down to the coordinated execution of a given set of driving operations. The assumption is substantiated by a compositionality result considering that autopilots are dynamic systems receiving a small number of types of driving configurations as input, each configuration defining a free space in its neighborhood. It is shown that safe driving for each type of configuration in the corresponding free space, implies safe driving for any possible scenario under some easy-to-check conditions concerning the transition between configurations. The designed autopilot comprises distinct control policies one per type of driving configurations, articulated in two consecutive phases. The first phase consists of carefully managing a potentially risky situation by virtually reducing speed, while the second phase consists of exiting the situation by accelerating. The autopilots designed use for their predictions simple functions characterizing the acceleration and deceleration capabilities of the vehicles. They cover the main driving operations, including entering a main road, overtaking, crossing intersections protected by traffic lights or signals, and driving on freeways. The results presented reinforce the case for solutions that incorporate mathematically elegant and robust decision methods that are safe by construction.

cs.MA↗

arXiv2026

Leveraging AI Agents for Autonomous Networks: A Reference Architecture and Empirical Studies

The evolution toward Level 4 (L4) Autonomous Networks (AN) represents a strategic inflection point in telecommunications, where networks must transcend reactive automation to achieve genuine cognitive capabilities--fulfilling TM Forum's vision of self-configuring, self-healing, and self-optimizing systems that deliver zero-wait, zero-touch, and zero-fault services. This work bridges the gap between architectural theory and operational reality by implementing Joseph Sifakis's AN Agent reference architecture in a functional cognitive system, deploying coordinated proactive-reactive runtimes driven by hybrid knowledge representation. Through an empirical case study of a Radio Access Network (RAN) Link Adaptation (LA) Agent, we validate this framework's transformative potential: demonstrating sub-10 ms real-time control in 5G NR sub-6 GHz while achieving 4% higher downlink throughput than Outer Loop Link Adaptation (OLLA) algorithms and 85% Block Error Rate (BLER) reduction for ultra-reliable services through dynamic Modulation and Coding Scheme (MCS) optimization. These improvements confirm the architecture's viability in overcoming traditional autonomy barriers and advancing critical L4-enabling capabilities toward next-generation objectives.

cs.AI↗

arXiv2025

Testing Autonomous Driving Systems -- What Really Matters and What Doesn't

Despite extensive research, the testing of autonomous driving systems (ADS) landscape remains fragmented, and there is currently no basis for an informed technical assessment of the importance and contribution of the current state of the art. This paper attempts to address this problem by exploring two complementary aspects. First, it proposes a framework for comparing existing test methods in terms of their intrinsic effectiveness and validity. It shows that many methods do not meet both of these requirements. Either because they are based on criteria that do not allow for rapid, inexpensive, and comprehensive detection of failures, or because the degree of validity of the properties tested cannot be accurately estimated. In particular, it is shown that most critical test methods do not take into account the nominal operational capabilities of autopilots and generate scenarios that are impossible for the tested vehicles to handle, resulting in unjustified rejections. Secondly, the paper shows that test effectiveness and validity are highly dependent on how autopilots are designed: how they choose between different control policies to perform maneuvers, as well as on the reproducibility of the results. In fact, most test methods take for granted two principles underlying traditional methods, but do not generally apply to ADS. We maintain that the absence of rationality and determinacy significantly impairs the effectiveness and validity of test methods, and provide test results on eight open autopilots, in which most do not satisfy these properties, thereby illustrating this fact. We conclude that under the current state of the art, it is impossible to obtain strong enough guarantees for essential autopilot properties and recommend that autopilots be developed with a view to both rationality and determinacy.

cs.SE↗

arXiv2025

A Comprehensive Evaluation of Four End-to-End AI Autopilots Using CCTest and the Carla Leaderboard

End-to-end AI autopilots for autonomous driving systems have emerged as a promising alternative to traditional modular autopilots, offering the potential to reduce development costs and mitigate defects arising from module composition. However, they suffer from the well-known problems of AI systems such as non-determinism, non-explainability, and anomalies. This naturally raises the question of their evaluation and, in particular, their comparison with existing modular solutions. This work extends a study of the critical configuration testing (CCTest) approach that has been applied to four open modular autopilots. This approach differs from others in that it generates test cases ensuring safe control policies are possible for the tested autopilots. This enables an accurate assessment of the ability to drive safely in critical situations, as any incident observed in the simulation involves the failure of a tested autopilot. The contribution of this paper is twofold. Firstly, we apply the CCTest approach to four end-to-end open autopilots, InterFuser, MILE, Transfuser, and LMDrive, and compare their test results with those of the four modular open autopilots previously tested with the same approach implemented in the Carla simulation environment. This comparison identifies both differences and similarities in the failures of the two autopilot types in critical configurations. Secondly, we compare the evaluations of the four autopilots carried out in the Carla Leaderboard with the CCTest results. This comparison reveals significant discrepancies, reflecting differences in test case generation criteria and risk assessment methods. It underlines the need to work towards the development of objective assessment methods combining qualitative and quantitative criteria.

cs.SE↗

arXiv2025

A Reference Architecture for Autonomous Networks: An Agent-Based Approach

The vision of autonomous systems is becoming increasingly important in many application areas, where the aim is to replace humans with agents. These include autonomous vehicles and other agents' applications in business processes and problem-solving. For networks, the increasing scale and operation and management (O&M) complexity drive the need for autonomous networks (AN). The technical objective of AN is to ensure trustworthy O&M without human intervention for higher efficiency and lower operating costs. However, realizing AN seems more difficult than autonomous vehicles. It encounters challenges of networks' structural and functional complexity, which operate as distributed dynamic systems governed by various technical and economic constraints. A key problem lies in formulating a rigorous development methodology that facilitates a seamless transition from traditional networks to AN. Central to this methodology is the definition of a reference architecture for network agents, which specifies the required functionalities for their realization, regardless of implementation choices. This article proposes a reference architecture characterizing main functional features, illustrating its application with network use cases. It shows how artificial intelligence components can be used to implement the required functionality and its coordination. The latter is achieved through the management and generation of shared domain-specific knowledge stored in long-term memory, ensuring the overall consistency of decisions and their execution. The article concludes with a discussion of architecture specialization for building network layer agents. It also identifies the main technical challenges ahead, such as satisfying essential requirements at development or runtime, as well as the issue of coordinating agents to achieve collective intelligence in meeting overall network goals.

cs.NI↗

arXiv2024

World Models: The Safety Perspective

With the proliferation of the Large Language Model (LLM), the concept of World Models (WM) has recently attracted a great deal of attention in the AI research community, especially in the context of AI agents. It is arguably evolving into an essential foundation for building AI agent systems. A WM is intended to help the agent predict the future evolution of environmental states or help the agent fill in missing information so that it can plan its actions and behave safely. The safety property of WM plays a key role in their effective use in critical applications. In this work, we review and analyze the impacts of the current state-of-the-art in WM technology from the point of view of trustworthiness and safety based on a comprehensive survey and the fields of application envisaged. We provide an in-depth analysis of state-of-the-art WMs and derive technical research challenges and their impact in order to call on the research community to collaborate on improving the safety and trustworthiness of WM.

cs.AI↗

arXiv2024

Rigorous Simulation-based Testing for Autonomous Driving Systems -- Targeting the Achilles' Heel of Four Open Autopilots

Simulation-based testing remains the main approach for validating Autonomous Driving Systems. We propose a rigorous test method based on breaking down scenarios into simple ones, taking into account the fact that autopilots make decisions according to traffic rules whose application depends on local knowledge and context. This leads us to consider the autopilot as a dynamic system receiving three different types of vistas as input, each characterizing a specific driving operation and a corresponding control policy. The test method for the considered vista types generates test cases for critical configurations that place the vehicle under test in critical situations characterized by the transition from cautious behavior to progression in order to clear an obstacle. The test cases thus generated are realistic, i.e., they determine the initial conditions from which safe control policies are possible, based on knowledge of the vehicle's dynamic characteristics. Constraint analysis identifies the most critical test cases, whose success implies the validity of less critical ones. Test coverage can therefore be greatly simplified. Critical test cases reveal major defects in Apollo, Autoware, and the Carla and LGSVL autopilots. Defects include accidents, software failures, and traffic rule violations that would be difficult to detect by random simulation, as the test cases lead to situations characterized by finely-tuned parameters of the vehicles involved, such as their relative position and speed. Our results corroborate real-life observations and confirm that autonomous driving systems still have a long way to go before offering acceptable safety guarantees.

cs.SE↗

arXiv2023

Testing System Intelligence

We discuss the adequacy of tests for intelligent systems and practical problems raised by their implementation. We propose the replacement test as the ability of a system to replace successfully another system performing a task in a given context. We show how it can characterize salient aspects of human intelligence that cannot be taken into account by the Turing test. We argue that building intelligent systems passing the replacement test involves a series of technical problems that are outside the scope of current AI. We present a framework for implementing the proposed test and validating the properties of the intelligent systems. We discuss the inherent limitations of intelligent system validation and advocate new theoretical foundations for extending existing rigorous test methods. We suggest that the replacement test, based on the complementarity of skills between human and machine, can lead to a multitude of intelligence concepts reflecting the ability to combine data-based and symbolic knowledge to varying degrees.

cs.AI↗

arXiv2023

Simulation-based Validation for Autonomous Driving Systems

Simulation is essential to validate autonomous driving systems. However, a simple simulation, even for an extremely high number of simulated miles or hours, is not sufficient. We need well-founded criteria showing that simulation does indeed cover a large fraction of the relevant real-world situations. In addition, the validation must concern not only incidents, but also the detection of any type of potentially dangerous situation, such as traffic violations. We investigate a rigorous simulation and testing-based validation method for autonomous driving systems that integrates an existing industrial simulator and a formally defined testing environment. The environment includes a scenario generator that drives the simulation process and a monitor that checks at runtime the observed behavior of the system against a set of system properties to be validated. The validation method consists in extracting from the simulator a semantic model of the simulated system including a metric graph, which is a mathematical model of the environment in which the vehicles of the system evolve. The monitor can verify properties formalized in a first-order linear temporal logic and provide diagnostics explaining their non satisfaction. Instead of exploring the system behavior randomly as many simulators do, we propose a method to systematically generate sets of scenarios that cover potentially risky situations, especially for different types of junctions where specific traffic rules must be respected. We show that the systematic exploration of risky situations has uncovered many flaws in the real simulator that would have been very difficult to discover by a random exploration process.

cs.SE↗

arXiv2022

Correct by Design Coordination of Autonomous Driving Systems

The paper proposes a method for the correct by design coordination of autonomous driving systems (ADS). It builds on previous results on collision avoidance policies and the modeling of ADS by combining descriptions of their static environment in the form of maps, and the dynamic behavior of their vehicles. An ADS is modeled as a dynamic system involving a set of vehicles coordinated by a Runtime that based on vehicle positions on a map and their kinetic attributes, computes free spaces for each vehicle. Vehicles are bounded to move within the corresponding allocated free spaces. We provide a correct by design safe control policy for an ADS if its vehicles and the Runtime respect corresponding assume-guarantee contracts. The result is established by showing that the composition of assume-guarantee contracts is an inductive invariant that entails ADS safety. We show that it is practically possible to define speed control policies for vehicles that comply with their contracts. Furthermore, we show that traffic rules can be specified in a linear-time temporal logic, as a class of formulas that constrain vehicle speeds. The main result is that, given a set of traffic rules, it is possible to derive free space policies of the Runtime such that the resulting system behavior is safe by design with respect to the rules.

cs.MA↗

arXiv2021

Verification of Component-based Systems with Recursive Architectures

We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the description of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. For parametric systems specified in this logic, we show that decision problems such as reaching deadlock or violating critical section are undecidable, in general. Despite this negative result, we provide for these decision problems practical semi-algorithms relying on the automatic synthesis of structural invariants allowing the proof of general safety properties. The invariants are defined using the WSkS fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection, thus reducing a verification problem to checking satisfiability of a WSkS formula.

cs.FL↗

arXiv2021

Runtime Safety Assurance for Learning-enabled Control of Autonomous Driving Vehicles

Providing safety guarantees for Autonomous Vehicle (AV) systems with machine-learning-based controllers remains a challenging issue. In this work, we propose Simplex-Drive, a framework that can achieve runtime safety assurance for machine-learning enabled controllers of AVs. The proposed Simplex-Drive consists of an unverified Deep Reinforcement Learning (DRL)-based advanced controller (AC) that achieves desirable performance in complex scenarios, a Velocity-Obstacle (VO) based baseline safe controller (BC) with provably safety guarantees, and a verified mode management unit that monitors the operation status and switches the control authority between AC and BC based on safety-related conditions. We provide a formal correctness proof of Simplex-Drive and conduct a lane-changing case study in dense traffic scenarios. The simulation experiment results demonstrate that Simplex-Drive can always ensure operation safety without sacrificing control performance, even if the DRL policy may lead to deviations from the safe status.

cs.RO↗

arXiv2021

Specification and Validation of Autonomous Driving Systems: A Multilevel Semantic Framework

Autonomous Driving Systems (ADS) are critical dynamic reconfigurable agent systems whose specification and validation raises extremely challenging problems. The paper presents a multilevel semantic framework for the specification of ADS and discusses associated validation problems. The framework relies on a formal definition of maps modeling the physical environment in which vehicles evolve. Maps are directed metric graphs whose nodes represent positions and edges represent segments of roads. We study basic properties of maps including their geometric consistency. Furthermore, we study position refinement and segment abstraction relations allowing multilevel representation from purely topological to detailed geometric. We progressively define first order logics for modeling families of maps and distributions of vehicles over maps. These are Configuration Logics, which in addition to the usual logical connectives are equipped with a coalescing operator to build configurations of models. We study their semantics and basic properties. We illustrate their use for the specification of traffic rules and scenarios characterizing sequences of scenes. We study various aspects of the validation problem including run-time verification and satisfiability of specifications. Finally, we show links of our framework with practical validation needs for ADS and advocate its adequacy for addressing the many facets of this challenge.

cs.MA↗

arXiv2021

Structural Invariants for the Verification of Systems with Parameterized Architectures

We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology of the system (e.g.\ pipeline, ring). The logic can be easily embedded in monadic second order logic of finitely many successors, and is therefore decidable. Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires to infer an inductive invariant that contains all reachable states of all system instances, and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions, without costly fixed point iterations. We experimentally prove that this invariant is strong enough to verify safety properties of a large number of systems including textbook examples (dining philosophers, synchronization schemes), classical mutual exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for an arbitrary number of components.

cs.DC↗

arXiv2021

A hybrid controller for safe and efficient collision avoidance control

We design and experimentally evaluate a hybrid safe-by-construction collision avoidance controller for autonomous vehicles. The controller combines into a single architecture the respective advantages of an adaptive controller and a discrete safe controller. The adaptive controller relies on model predictive control to achieve optimal efficiency in nominal conditions. The safe controller avoids collision by applying two different policies, for nominal and out-of-nominal conditions, respectively. We present design principles for both the adaptive and the safe controller and show how each one can contribute in the hybrid architecture to improve performance, road occupancy and passenger comfort while preserving safety. The experimental results confirm the feasibility of the approach and the practical relevance of hybrid controllers for safe and efficient driving.

cs.RO↗

arXiv2020

Safe and efficient collision avoidance control for autonomous vehicles

We study a novel principle for safe and efficient collision avoidance that adopts a mathematically elegant and general framework abstracting as much as possible from the controlled vehicle's dynamics and of its environment. Vehicle dynamics is characterized by pre-computed functions for accelerating and braking to a given speed. Environment is modeled by a function of time giving the free distance ahead of the controlled vehicle under the assumption that the obstacles are either fixed or are moving in the same direction. The main result is a control policy enforcing the vehicle's speed so as to avoid collision and efficiently use the free distance ahead, provided some initial safety condition holds. The studied principle is applied to the design of two discrete controllers, one synchronous and another asynchronous. We show that both controllers are safe by construction. Furthermore, we show that their efficiency strictly increases for decreasing granularity of discretization. We present implementations of the two controllers, their experimental evaluation in the Carla autonomous driving simulator and investigate various performance issues.

eess.SY↗

arXiv2019

Autonomics: In Search of a Foundation for Next Generation Autonomous Systems

The potential benefits of autonomous systems have been driving intensive development of such systems, and of supporting tools and methodologies. However, there are still major issues to be dealt with before such development becomes commonplace engineering practice, with accepted and trustworthy deliverables. We argue that a solid, evolving, publicly available, community-controlled foundation for developing next generation autonomous systems is a must. We discuss what is needed for such a foundation, identify a central aspect thereof, namely, decision-making, and focus on three main challenges: (i) how to specify autonomous system behavior and the associated decisions in the face of unpredictability of future events and conditions and the inadequacy of current languages for describing these; (ii) how to carry out faithful simulation and analysis of system behavior with respect to rich environments that include humans, physical artifacts, and other systems,; and (iii) how to engineer systems that combine executable model-driven techniques and data-driven machine learning techniques. We argue that autonomics, i.e., the study of unique challenges presented by next generation autonomous systems, and research towards resolving them, can introduce substantial contributions and innovations in system engineering and computer science.

cs.SE↗