1,720,990 research outputs found
Conditional Simple Temporal Networks with Uncertainty and Decisions
Full text linkA conditional simple temporal network with uncertainty (CSTNU) is a framework able to model temporal plans subject to both conditional constraints and uncertain durations. The combination of these two characteristics represents the uncontrollable part of the network. That is, before the network starts executing, we do not know completely which time points and constraints will be taken into consideration nor how long the uncertain durations will last. Dynamic controllability (DC) implies the existence of a strategy scheduling the time points of the network in real time depending on how the uncontrollable part behaves. Despite all this, CSTNUs fail to model temporal plans in which a few conditional constraints are under control and may therefore influence (or be influenced by) the uncontrollable part. To bridge this gap, this paper proposes conditional simple temporal networks with uncertainty and decisions (CSTNUDs) which introduce decision time points into the specification in order to operate on this conditional part under control. We model the dynamic controllability checking (DC-checking) of a CSTNUD as a two-player game in which each player makes his moves in his turn at a specific time instant. We give an encoding into timed game automata for a sound and complete DC-checking. We also synthesize memoryless execution strategies for CSTNUDs proved to be DC. The proposed approach is fully automated
Temporal and Resource Controllability of Workflows Under Uncertainty
Full text linkWorkflow technology has long been employed for the modeling, validation and execution of business processes. A workflow is a formal description of a business process in which single atomic work units (tasks), organized in a partial order, are assigned to processing entities (agents) in order to achieve some business goal(s). Workflows can also employ workflow paths (projections with respect to a total truth value assignment to the Boolean variables associated to the conditional split connectors) in order (not) to execute a subset of tasks. A workflow management system coordinates the execution of tasks that are part of workflow instances such that all relevant constraints are eventually satisfied. Temporal workflows specify business processes subject to temporal constraints such as controllable or uncontrollable durations, delays and deadlines. The choice of a workflow path may be controllable or not, considered either in isolation or in combination with uncontrollable durations. Access controlled workflows specify workflows in which users are authorized for task executions and authorization constraints say which users remain authorized to execute which tasks depending on who did what. Access controlled workflows may consider workflow paths too other than the uncertain availability of resources (users, throughout this thesis). When either a task duration or the choice of the workflow path to take or the availability of a user is out of control, we need to verify that the workflow can be executed by verifying all constraints for any possible combination of behaviors arising from the uncontrollable parts. Indeed, users might be absent before starting the execution (static resiliency), they can also become so during execution (decremental resiliency) or they can come and go throughout the execution (dynamic resiliency). Temporal access controlled workflows merge the two previous formalisms by considering several kinds of uncontrollable parts simultaneously. Authorization constraints may be extended to support conditional and temporal features. A few years ago some proposals addressed the temporal controllability of workflows by encoding them into temporal networks to exploit "off-the-shelf" controllability checking algorithms available for them. However, those proposals fail to address temporal controllability where the controllable and uncontrollable choices of workflow paths may mutually influence one another. Furthermore, to the best of my knowledge, controllability of access controlled workflows subject to uncontrollable workflow paths and algorithms to validate and execute dynamically resilient workflows remain unexplored. To overcome these limitations, this thesis goes for exact algorithms by addressing temporal and resource controllability of workflows under uncertainty. I provide several new classes of (temporal) constraint networks and corresponding algorithms to check their controllability. After that, I encode workflows into these new formalisms. I also provide an encoding into instantaneous timed games to model static, decremental and dynamic resiliency and synthesize memoryless execution strategies. I developed a few tools with which I carried out some initial experimental evaluations
Dynamic controllability of temporal networks with instantaneous reaction
No full textA Conditional Simple Temporal Network with Uncertainty and Decisions (CSTNUD) is a formalism to model, validate, and execute temporal plans subject to controllable and uncontrollable events as well as controllable and uncontrollable choices simultaneously. Dynamic Controllability implies the existence of a strategy scheduling the events and fixing the controllable choices in real time in a way that only depends on the already executed uncontrollable events and already fixed uncontrollable choices. This paper unifies CSTNUDs with other temporal network formalisms by providing Conditional Temporal Networks with Uncertainty and Decisions (CTNUDs) and proposes a semantics for dynamic controllability modeled as a two-player game between Controller and Nature where each player can react instantaneously to the other player moves. Such a game is designed to guarantee termination with exactly one winner (i.e., the game is determined). We prove that adopting the instantaneous reaction semantics allows for modeling any possible reaction time, absorbing de facto previous proposed semantics of dynamic controllability. We provide an encoding into Timed Game Automata to synthesize an execution strategy for any dynamically controllable CTNUD. We implement our approach to synthesize C++ programs for the execution of dynamically controllable CTNUDs. We test our software on a set of randomly-generated instances
Dynamic controllability of temporal networks with instantaneous reaction
No full textA Conditional Simple Temporal Network with Uncertainty and Decisions (CSTNUD) is a for- malism to model, validate, and execute temporal plans subject to controllable and uncon- trollable events as well as controllable and uncontrollable choices simultaneously. Dynamic Controllability implies the existence of a strategy scheduling the events and fixing the controllable choices in real time in a way that only depends on the already executed uncontrollable events and already fixed uncontrollable choices. This paper unifies CSTNUDs with other temporal network formalisms by providing Conditional Temporal Networks with Uncertainty and Decisions (CTNUDs) and proposes a semantics for dynamic controllability modeled as a two-player game between Controller and Nature where each player can react instantaneously to the other player moves. Such a game is designed to guarantee termination with exactly one winner (i.e., the game is determined). We prove that adopting the instantaneous reaction semantics allows for modeling any possible reaction time, absorbing de facto previous proposed semantics of dynamic controllability. We provide an encoding into Timed Game Automata to synthesize an execution strategy for any dynamically controllable CTNUD. We implement our approach to synthesize C++ programs for the execution of dynamically controllable CTNUDs. We test our software on a set of randomly-generated instances
Repair of Unsound Data-Aware Process Models
No full textProcess-aware Information Systems support the enactment of business processes, and rely on a model that prescribes which executions are allowed. As a result, the model needs to be sound for the process to be carried out. Traditionally, soundness has been defined and studied by only focusing on the control-flow. Some works proposed techniques to repair the process model to ensure soundness, ignoring data and decision perspectives. This paper puts forward a technique to repair the data perspective of process models, keeping intact the control flow structure. Processes are modeled by acyclic Data Petri Nets. Our approach repairs the Constraint Graph, a finite symbolic abstraction of the infinite state-space of the underlying Data Petri Net. The changes in the Constraint Graph are then projected back onto the Data Petri Net
Reducing the Number of Disjuncts in DTPs
No full textThe Disjunctive Temporal Problem (DTP) consists of a finite set of time points and a finite set of constraints, each composed of alternative disjuncts modeling delays and deadlines for possibly different pairs of time points. An instance of DTP is consistent if there exists an assignment of real values to the time points such that all constraints are satisfied. Here we focus on DTPs with at most k >= 2 disjuncts per constraint. We define a few polynomial-time encoders to reduce the number of disjuncts to at most k', with 2 <= k' <= k, preserving (in)consistency of the original instance. These results generalize previous work in the literature. Anyway, we provide a methodology not related to any specific technology that sticks to DTP
Mining CSTNUDs significant for a set of traces is polynomial
No full textA Conditional Simple Temporal Network with Uncertainty and Decisions (CSTNUD) is a formalism for temporal plans that models controllable and uncontrollable durations as well as controllable and uncontrollable choices simultaneously. In the classic top-down model-based engineering approach, a designer builds CSTNUDs to model, validate and execute some temporal plans of interest. In this paper, we investigate a bottom-up approach by providing a deterministic polynomial time algorithm to mine a CSTNUD from a set of execution traces (i.e., a log). We provide a prototype implementation and we test it with a set of artificial data. Finally, we elaborate on consistency and controllability of mined networks
Automated Synthesis of Certified Neural Networks
Full text linkNeural networks find applications in many safety-critical systems that raise concerns about their deployment: Are we sure the network will never advise doing anything violating a set of safety constraints? Formal verification has been recently applied to prove whether an existing neural network is certified for some property (i.e., if it satisfies the property for all possible inputs) or not. Formal verification can prove that a network respects the property, but cannot fix a network that does not respect it. In this paper we focus on the automated synthesis of certified neural networks, that is, on how to automatically build a network that is guaranteed to respect some required properties. We exploit a Counter Example Guided Inductive Synthesis (CEGIS) loop that alternates Deep Learning, Formal Verification, and a novel data generation technique that augments the training data to synthesize certified networks in a fully automatic way. An application of a proof-of-concept implementation of the framework shows the feasibility of the approach
Resource Controllability of Workflows Under Conditional Uncertainty
No full textAn access controlled workflow (ACWF) specifies a set of tasks that have to be executed by authorized users with respect to some partial order in a way that all authorization constraints are satisfied. Recent research focused on weak, strong and dynamic controllability of ACWFs under conditional uncertainty showing that directional consistency is a way to generate any consistent assignment of tasks to users efficiently and without backtracking. This means that during execution we never realize that we would have chosen a different user for some previous task to avoid some constraint violation. However, dynamic controllability of ACWFs also depends on how the components of the ACWF are totally ordered. In this paper, we employ Constraint Networks Under Conditional Uncertainty (CNCUs) to solve this limitation, and provide an encoding from ACWFs into CNCUs to exploit existing controllability checking algorithms for CNCUs. We also address the execution of a controllable ACWF discussing which (possibly different) users are committed for the same tasks depending on what is going on (online planning)
Conditional simple temporal networks with uncertainty and decisions
Full text linkA Conditional Simple Temporal Network with Uncertainty (CSTNU) is a formalism able to model temporal plans subject to both conditional constraints and uncertain durations. The combination of these two characteristics represents the uncontrollable part of the network. That is, before the network starts executing, we do not know completely which time points and constraints will be taken into consideration nor how long the uncertain durations will last. Dynamic Controllability (DC) implies the existence of a strategy scheduling the time points of the network in real time depending on how the uncontrollable part behaves. Despite all this, CSTNUs fail to model temporal plans in which a few conditional constraints are under control and may therefore influence (or be influenced by) the uncontrollable part. To bridge this gap, this paper proposes Conditional Simple Temporal Networks with Uncertainty and Decisions (CSTNUDs) which introduce decision time points into the specification in order to operate on this conditional part under control. We model the dynamic controllability checking (DC-checking) of a CSTNUD as a two-player game in which each player makes his moves in his turn at a specific time instant. We give an encoding into timed game automata for a sound and complete DC-checking. We also synthesize memoryless execution strategies for CSTNUDs proved to be DC and carry out an experimental evaluation with Esse, a tool that we have designed for CSTNUDs to make the approach fully automated
- …
