Collaborative Research:CPS:Medium:ASTrA:Automated Synthesis for Trustworthy Autonomous Utility Services
项目来源
项目主持人
项目受资助机构
项目编号
财政年度
立项时间
研究期限
项目级别
受资助金额
学科
学科代码
基金类别
关键词
参与者
参与机构
人员信息
机构信息
项目主管部门
项目官员
1.Passivity tools for hybrid learning rules in large populations
- 关键词:
- Asymptotic stability;Cones;Intelligent agents;Learning systems;Stabilization;System theory;Asymptotic stabilization;Distributed learning;Equilibrium stability;Evolutionary dynamics;Hybrid learning rule;Large population;Learning rules;Multiagent systems (MASs);Strategic interactions;System-theoretic passivity
- Certório, Jair;Chang, Kevin;Martins, Nuno C.;Nuzzo, Pierluigi;Shoukry, Yasser
- 《Automatica》
- 2026年
- 187卷
- 期
- 期刊
Recent work has pioneered the use of system-theoretic passivity to study equilibrium stability for the dynamics of noncooperative strategic interactions in large populations of learning agents. In this and related works, the stability analysis leverages knowledge that certain "canonical" classes of learning rules used to model the agents’ strategic behaviors satisfy a passivity condition known as δ-passivity. In this paper, we consider that agents exhibit learning behaviors that do not align with a canonical class. Specifically, we focus on characterizing δ-passivity for hybrid learning rules that combine elements from canonical classes. Our analysis also introduces and uses a more general version of δ-passivity, which, for the first time, can handle discontinuous learning rules, including those showing best response behaviors. We state and prove theorems establishing δ-passivity for two broad convex cones of hybrid learning rules. These cones can merge into a larger one preserving δ-passivity in scenarios limited to two strategies. In our proofs, we establish intermediate facts that are significant on their own and could potentially be used to further generalize our work. We illustrate the applicability of our results through numerical examples. © 2026 The Author(s)
...2.Contract Embeddings for Layered Control Architectures
- 关键词:
- Formal methods; layered control architectures; contract-based design;safe control; correct-by-construction design;DESIGN; VALIDATION; FRAMEWORK; SYSTEMS; LOGIC
- Naik, Nikhil Vijay;Pinto, Alessandro;Nuzzo, Pierluigi
- 《ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS》
- 2025年
- 24卷
- 5期
- 期刊
The design of complex cyber-physical system architectures is often hierarchical. System specifications are mapped to an implementation layer via a stepwise refinement process involving multiple intermediate layers. These layers may capture different functionalities, and the orchestration of a variety of heterogeneous techniques suited to each layer may be required to achieve the overall design objectives. Due to their heterogeneity, ensuring traceability and verifiability of such architectures is a challenging problem. In this article, we present a correct-by-construction methodology for designing heterogeneous layered architectures. We capture the specifications at each layer with assume-guarantee contracts, a specification paradigm which can encompass a variety of modeling formalisms. We then use the notion of contract embeddings to define specification refinement, rigorously and traceably mapping specifications across layers modeled with heterogeneous formalisms. We instantiate our methodology on the design of layered control architectures (LCAs), resulting in a novel approach that can verifiably orchestrate domain-specific techniques to satisfy both global planning and local safety requirements. In the context of LCAs, we derive necessary conditions for correct specification refinement and results for compositional realization of control safety specifications. We illustrate our design methodology on a motivating example and a case study derived from robotic mission planning and control.
...3.Constraint-driven nonlinear reachability analysis with automated tuning of tool properties
- 关键词:
- Cost functions;Nonlinear analysis;Optimization;Automated tuning;Optimisations;Property;Property value;Reachability analysis;Reachable set;Rigorous numerics;Safety verification;Specific properties;Tool automation
- Geretti, Luca;Collins, Pieter;Nuzzo, Pierluigi;Villa, Tiziano
- 《Nonlinear Analysis: Hybrid Systems》
- 2024年
- 54卷
- 期
- 期刊
The effectiveness of reachability analysis often depends on choosing appropriate values for a set of tool-specific properties which need to be manually tailored to the specific system involved and the reachable set to be evolved. Such property tuning is a time-consuming task, especially when dealing with nonlinear systems. In this paper, we propose, instead, a methodology to automatically and dynamically choose property values for reachability analysis along the system evolution, based on the actual verification objective, i.e., the verification or falsification of a set of constraints. By leveraging an initial solution to the reachable set, we estimate bounds on the numerical accuracy required from each integration step to provide a definite answer to the satisfaction of the constraints. Based on these accuracy bounds, we design a cost function which we use, after mapping the property space to an integer space, to search for locally optimal property values that yield the desired accuracy. Results from the application of our methodology to the nonlinear reachability analysis tool ARIADNE show that the frequency of correct answers to constraint satisfaction problems increases significantly with respect to a manual approach. © 2024 The Authors
...4.Optimal Control of Logically Constrained Partially Observable and Multi-Agent Markov Decision Processes
- 关键词:
- Behavioral research;Computer circuits;Decision theory;Job analysis;Multi agent systems;Process control;Robot programming;Stochastic control systems;Stochastic systems;Temporal logic;Logic;Logical constraints;Markov Decision Processes;Multi-agent markov decision process;Operational requirements;Optimal controls;Partially observable Markov decision process;Stochastic optimal control;Task analysis
- Kalagarla, Krishna C.;Kartik, Dhruva;Shen, Dongming;Jain, Rahul;Nayyar, Ashutosh;Nuzzo, Pierluigi
- 《IEEE Transactions on Automatic Control》
- 2024年
- 卷
- 期
- 期刊
Autonomous systems often have logical constraints arising, for example, from safety, operational, or regulatory requirements. Such constraints can be expressed using temporal logic specifications. The system state is often partially observable. Moreover, it could encompass a team of multiple agents with a common objective but disparate information structures and constraints. In this paper, we first introduce an optimal control theory for partially observable Markov decision processes (POMDPs) with finite linear temporal logic ($\boldsymbol{LTL}_{\bf f}$) constraints. We provide a structured methodology for synthesizing policies that maximize a cumulative reward while ensuring that the probability of satisfying a temporal logic constraint is sufficiently high. Our approach comes with guarantees on approximate reward optimality and constraint satisfaction. We then build on this approach to design an optimal control framework for logically constrained multi-agent settings with information asymmetry. We illustrate the effectiveness of our approach by implementing it on several case studies. IEEE
...5.Contract-Based Hierarchical Modeling and Traceability of Heterogeneous Requirements
- 关键词:
- Integrated circuit design;Smart contract;Complex mission;Contract-based designs;Cybe-physical systems;Cyber-physical systems;Embeddings;Hierarchical model;Mission critical systems;Model-based design;Requirements formalizations;Traceability validation
- Naik, Nikhil Vijay;Pinto, Alessandro;Nuzzo, Pierluigi
- 《IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems》
- 2024年
- 卷
- 期
- 期刊
The design of complex mission-critical systems often follows a layered approach, which may lead to complicated, multi-level, multi-viewpoint requirement hierarchies. This heterogeneity makes it challenging to guarantee the traceability of the requirements across levels of abstraction and, consequently, the satisfaction of the requirements by a system implementation, especially when requirements at different abstraction levels are expressed using different mathematical formalisms and modeling languages. In this paper, we address this challenge by introducing heterogeneous hierarchical contract networks (HHCNs), a formal model based on a graph of assume-guarantee contracts, for capturing and analyzing heterogeneous requirement hierarchies. We formulate the requirement traceability validation problem in terms of contract refinement relations between nodes in an HHCN. We then define contract embeddings to enable reasoning about refinements across levels of abstraction in the HHCN that are expressed using heterogeneous formalisms. Contract embeddings leverage the notion of conservative approximation to rigorously map contracts across levels of abstraction while ensuring that refinement is preserved independently of the formalism to which the contracts are mapped. We illustrate their effectiveness on a case study motivated by a multi-agent autonomous lunar rover mission. © 1982-2012 IEEE.
...
