Collaborative Research:CPS:Medium:ASTrA:Automated Synthesis for Trustworthy Autonomous Utility Services

项目来源

美国国家科学基金(NSF)

项目主持人

Pierluigi Nuzzo

项目受资助机构

UNIVERSITY OF CALIFORNIA BERKELEY

项目编号

2514683

财政年度

2025,2021

立项时间

未公开

研究期限

未知 / 未知

项目级别

国家级

受资助金额

534361.00美元

学科

未公开

学科代码

未公开

基金类别

Standard Grant

关键词

CPS-Cyber-Physical Systems ; CYBER-PHYSICAL SYSTEMS(CPS)

参与者

未公开

参与机构

REGENTS OF THE UNIVERSITY OF CALIFORNIA,THE

项目标书摘要:Large-scale systems with societal relevance,such as power generation systems,are increasingly able to leverage new technologies to mitigate their environmental impact,e.g.,by harvesting energy from renewable sources.This NSF CPS project aims to investigate methods and computational tools to design a new user-centric paradigm for energy apportionment and distribution and,more broadly,for trustworthy utility services.In this paradigm,distributed networked systems will assist the end users of electricity in scheduling and apportioning their consumption.Further,they will enable local and national utility managers to optimize the use of green energy sources while mitigating the effects of intermittence,promote fairness,equity,and affordability.This project pursues a tractable approach to address the challenges of modeling and designing these large-scale,mixed-autonomy,multi-agent CPSs.The intellectual merits include new scalable methods,algorithms,and tools for the design of distributed decision-making strategies and system architectures that can assist the end users in meeting their goals while guaranteeing compliance with the fairness,reliability,and physical constraints of the design.The broader impacts include enabling the automated design of distributed CPSs that coordinate their decision-making in many applications,from robotic swarms to smart manufacturing and smart cities.The research outcomes will also be used in K-12 and undergraduate STEM outreach efforts.The proposed framework,termed Automated Synthesis for Trustworthy Autonomous Utility Services(ASTrA),addresses the design challenges via a three-pronged approach.It uses population games to model the effect of distributed decision-making infrastructures(DMI)on large populations of strategic agents.DMIs will be realized via dedicated networked hybrid hardware architectures and algorithms we seek to design.ASTrA further introduces a systematic,layered methodology to automate the design,verification,and validation of DMIs from expressive representations of the requirements.Finally,it offers a set of cutting-edge computational tools to facilitate our methodology by enabling efficient reasoning about the interaction between discrete models,e.g.,used to describe complex missions or embedded software components,and continuous models used to describe physical processes.The evaluation plan involves experimentation on a real testbed designed for zero-net-energy applications.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

人员信息

Pierluigi Nuzzo(Principal Investigator):nuzzo@eecs.berkeley.edu;

机构信息

【University of California-Berkeley(Performance Institution)】StreetAddress:1608 4TH ST STE 201,BERKELEY,California,United States/ZipCode:947101749;【REGENTS OF THE UNIVERSITY OF CALIFORNIA,THE】StreetAddress:119 CALIFORNIA HALL,BERKELEY,California,United States/PhoneNumber:5106433891/ZipCode:947201509;

项目主管部门

Directorate for Engineering(ENG)-Division of Electrical,Communications and Cyber Systems(ECCS)

项目官员

Eyad Abed(Email:eabed@nsf.gov;Phone:7032922303)

  • 排序方式:
  • 1
  • /
  • 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.

    ...
  • 排序方式:
  • 1
  • /