Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements
- URL: http://arxiv.org/abs/2404.01858v1
- Date: Tue, 2 Apr 2024 11:36:58 GMT
- Title: Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements
- Authors: Tom Yaacov, Achiya Elyasaf, Gera Weiss,
- Abstract summary: We propose an idiom for tagging states with "must-finish," indicating that tasks are yet to be completed.
We also offer semantics and two execution mechanisms, one based on a translation to B"uchi automata and the other based on a Markov decision process (MDP)
- Score: 2.4387555567462647
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: One of the benefits of using executable specifications such as Behavioral Programming (BP) is the ability to align the system implementation with its requirements. This is facilitated in BP by a protocol that allows independent implementation modules that specify what the system may, must, and must not do. By that, each module can enforce a single system requirement, including negative specifications such as "don't do X after Y." The existing BP protocol, however, allows only the enforcement of safety requirements and does not support the execution of liveness properties such as "do X at least three times." To model liveness requirements in BP directly and independently, we propose idioms for tagging states with "must-finish," indicating that tasks are yet to be completed. We show that this idiom allows a direct specification of known requirements patterns from the literature. We also offer semantics and two execution mechanisms, one based on a translation to B\"uchi automata and the other based on a Markov decision process (MDP). The latter approach offers the possibility of utilizing deep reinforcement learning (DRL) algorithms, which bear the potential to handle large software systems effectively. This paper presents a qualitative and quantitative assessment of the proposed approach using a proof-of-concept tool. A formal analysis of the MDP-based execution mechanism is given in an appendix.
Related papers
- Towards an Enforceable GDPR Specification [49.1574468325115]
Privacy by Design (PbD) is prescribed by modern privacy regulations such as the EU's.
One emerging technique to realize PbD is enforcement (RE)
We present a set of requirements and an iterative methodology for creating formal specifications of legal provisions.
arXiv Detail & Related papers (2024-02-27T09:38:51Z) - LLM-based policy generation for intent-based management of applications [8.938462415711674]
We propose a pipeline that progressively decomposes intents by generating the required actions using a policy-based abstraction.
This allows us to automate the policy execution by creating a closed control loop for the intent deployment.
We evaluate our proposal with a use-case to fulfill and assure an application service chain of virtual network functions.
arXiv Detail & Related papers (2024-01-22T15:37:04Z) - Conformance Checking for Pushdown Reactive Systems based on Visibly
Pushdown Languages [0.0]
Testing pushdown reactive systems is deemed important to guarantee a precise and robust software development process.
We show that test suites with a complete fault coverage can be generated using this conformance relation for pushdown reactive systems.
arXiv Detail & Related papers (2023-08-14T14:37:43Z) - Towards Semantic Communication Protocols: A Probabilistic Logic
Perspective [69.68769942563812]
We propose a semantic protocol model (SPM) constructed by transforming an NPM into an interpretable symbolic graph written in the probabilistic logic programming language (ProbLog)
By leveraging its interpretability and memory-efficiency, we demonstrate several applications such as SPM reconfiguration for collision-avoidance.
arXiv Detail & Related papers (2022-07-08T14:19:36Z) - Reinforcement Learning for Task Specifications with Action-Constraints [4.046919218061427]
We propose a method to learn optimal control policies for a finite-state Markov Decision Process.
We assume that the set of action sequences that are deemed unsafe and/or safe are given in terms of a finite-state automaton.
We present a version of the Q-learning algorithm for learning optimal policies in the presence of non-Markovian action-sequence and state constraints.
arXiv Detail & Related papers (2022-01-02T04:22:01Z) - Pointwise Feasibility of Gaussian Process-based Safety-Critical Control
under Model Uncertainty [77.18483084440182]
Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are popular tools for enforcing safety and stability of a controlled system, respectively.
We present a Gaussian Process (GP)-based approach to tackle the problem of model uncertainty in safety-critical controllers that use CBFs and CLFs.
arXiv Detail & Related papers (2021-06-13T23:08:49Z) - Modular Deep Reinforcement Learning for Continuous Motion Planning with
Temporal Logic [59.94347858883343]
This paper investigates the motion planning of autonomous dynamical systems modeled by Markov decision processes (MDP)
The novelty is to design an embedded product MDP (EP-MDP) between the LDGBA and the MDP.
The proposed LDGBA-based reward shaping and discounting schemes for the model-free reinforcement learning (RL) only depend on the EP-MDP states.
arXiv Detail & Related papers (2021-02-24T01:11:25Z) - SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
We study the verification of parameterised multi-agent systems (MASs)
In particular, we study whether unwanted states, characterised as a given state formula, are reachable in a given MAS.
arXiv Detail & Related papers (2020-08-11T15:24:05Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs)
The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
arXiv Detail & Related papers (2019-02-02T20:09:32Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.