-
Model-Free Reinforcement Learning for Symbolic Automata-encoded Objectives
Authors:
Anand Balakrishnan,
Stefan Jakšić,
Edgar A. Aguilar,
Dejan Ničković,
Jyotirmoy V. Deshmukh
Abstract:
Reinforcement learning (RL) is a popular approach for robotic path planning in uncertain environments. However, the control policies trained for an RL agent crucially depend on user-defined, state-based reward functions. Poorly designed rewards can lead to policies that do get maximal rewards but fail to satisfy desired task objectives or are unsafe. There are several examples of the use of formal…
▽ More
Reinforcement learning (RL) is a popular approach for robotic path planning in uncertain environments. However, the control policies trained for an RL agent crucially depend on user-defined, state-based reward functions. Poorly designed rewards can lead to policies that do get maximal rewards but fail to satisfy desired task objectives or are unsafe. There are several examples of the use of formal languages such as temporal logics and automata to specify high-level task specifications for robots (in lieu of Markovian rewards). Recent efforts have focused on inferring state-based rewards from formal specifications; here, the goal is to provide (probabilistic) guarantees that the policy learned using RL (with the inferred rewards) satisfies the high-level formal specification. A key drawback of several of these techniques is that the rewards that they infer are sparse: the agent receives positive rewards only upon completion of the task and no rewards otherwise. This naturally leads to poor convergence properties and high variance during RL. In this work, we propose using formal specifications in the form of symbolic automata: these serve as a generalization of both bounded-time temporal logic-based specifications as well as automata. Furthermore, our use of symbolic automata allows us to define non-sparse potential-based rewards which empirically shape the reward surface, leading to better convergence during RL. We also show that our potential-based rewarding strategy still allows us to obtain the policy that maximizes the satisfaction of the given specification.
△ Less
Submitted 24 February, 2022; v1 submitted 4 February, 2022;
originally announced February 2022.
-
An Algebraic Framework for Runtime Verification
Authors:
Stefan Jaksic,
Ezio Bartocci,
Radu Grosu,
Dejan Nickovic
Abstract:
Runtime verification (RV) is a pragmatic and scalable, yet rigorous technique, to assess the correctness of complex systems, including cyber-physical systems (CPS). By measuring how robustly a CPS run satisfies a specification, RV allows in addition, to quantify the resiliency of a CPS to perturbations. In this paper we propose Algebraic Runtime Verification (ARV), a general, semantic framework fo…
▽ More
Runtime verification (RV) is a pragmatic and scalable, yet rigorous technique, to assess the correctness of complex systems, including cyber-physical systems (CPS). By measuring how robustly a CPS run satisfies a specification, RV allows in addition, to quantify the resiliency of a CPS to perturbations. In this paper we propose Algebraic Runtime Verification (ARV), a general, semantic framework for RV, which takes advantage of the monoidal structure of runs (w.r.t. concatenation) and the semiring structure of a specification automaton (w.r.t. choice and concatenation), to compute in an incremental and application specific fashion the resiliency measure. This allows us to expose the core aspects of RV, by develo** an abstract monitoring algorithm, and to strengthen and unify the various qualitative and quantitative approaches to RV, by instantiating choice and concatenation with real-valued functions as dictated by the application. We demonstrate the power and effectiveness of our framework on two case studies from the automotive domain.
△ Less
Submitted 11 February, 2018;
originally announced February 2018.
-
A Typed Model for Dynamic Authorizations
Authors:
Silvia Ghilezan,
Svetlana Jakšić,
Jovanka Pantović,
Jorge A. Pérez,
Hugo Torres Vieira
Abstract:
Security requirements in distributed software systems are inherently dynamic. In the case of authorization policies, resources are meant to be accessed only by authorized parties, but the authorization to access a resource may be dynamically granted/yielded. We describe ongoing work on a model for specifying communication and dynamic authorization handling. We build upon the pi-calculus so as to e…
▽ More
Security requirements in distributed software systems are inherently dynamic. In the case of authorization policies, resources are meant to be accessed only by authorized parties, but the authorization to access a resource may be dynamically granted/yielded. We describe ongoing work on a model for specifying communication and dynamic authorization handling. We build upon the pi-calculus so as to enrich communication-based systems with authorization specification and delegation; here authorizations regard channel usage and delegation refers to the act of yielding an authorization to another party. Our model includes: (i) a novel sco** construct for authorization, which allows to specify authorization boundaries, and (ii) communication primitives for authorizations, which allow to pass around authorizations to act on a given channel. An authorization error may consist in, e.g., performing an action along a name which is not under an appropriate authorization scope. We introduce a ty** discipline that ensures that processes never reduce to authorization errors, even when authorizations are dynamically delegated.
△ Less
Submitted 10 February, 2016;
originally announced February 2016.
-
Precise subty** for synchronous multiparty sessions
Authors:
Mariangiola Dezani-Ciancaglini,
Silvia Ghilezan,
Svetlana Jakšić,
Jovanka Pantović,
Nobuko Yoshida
Abstract:
The notion of subty** has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subty**, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with r…
▽ More
The notion of subty** has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subty**, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subty** for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness.
△ Less
Submitted 10 February, 2016;
originally announced February 2016.
-
Dynamic Role Authorization in Multiparty Conversations
Authors:
Silvia Ghilezan,
Svetlana Jakšić,
Jovanka Pantović,
Jorge A. Pérez,
Hugo Torres Vieira
Abstract:
Protocol specifications often identify the roles involved in communications. In multiparty protocols that involve task delegation it is often useful to consider settings in which different sites may act on behalf of a single role. It is then crucial to control the roles that the different parties are authorized to represent, including the case in which role authorizations are determined only at ru…
▽ More
Protocol specifications often identify the roles involved in communications. In multiparty protocols that involve task delegation it is often useful to consider settings in which different sites may act on behalf of a single role. It is then crucial to control the roles that the different parties are authorized to represent, including the case in which role authorizations are determined only at runtime. Building on previous work on conversation types with flexible role assignment, here we report initial results on a typed framework for the analysis of multiparty communications with dynamic role authorization and delegation. In the underlying process model, communication prefixes are annotated with role authorizations and authorizations can be passed around. We extend the conversation type system so as to statically distinguish processes that never incur in authorization errors. The proposed static discipline guarantees that processes are always authorized to communicate on behalf of an intended role, also covering the case in which authorizations are dynamically passed around in messages.
△ Less
Submitted 25 August, 2014;
originally announced August 2014.
