Free logic and infinite constraint networks

AbstractA current research problem in the area of business process management deals with the specification and checking of constraints on resources (e.g., users, agents, autonomous systems, etc.) allowed to be committed for the execution of specific tasks. Indeed, in many real-world situations, role assignments are not enough to assign tasks to the suitable resources. It could be the case that further requirements need to be specified and satisfied. As an example, one would like to avoid that employees that are relatives are assigned to a set of critical tasks in the same process in order to prevent fraud. The formal specification of a business process and its related access control constraints is obtained through a decoration of a classic business process with roles, users, and constraints on their commitment. As a result, such a process specifies a set of tasks that need to be executed by authorized users with respect to some partial order in a way that all authorization constraints are satisfied. Controllability refers in this case to the capability of executing the process satisfying all these constraints, even when some process components, e.g., gateway conditions, can only be observed, but not decided, by the process engine responsible of the execution. In this paper, we propose conditional constraint networks with decisions (CCNDs) as a model to encode business processes that involve access control and conditional branches that may be both controllable and uncontrollable. We define weak, strong, and dynamic controllability of CCNDs as two-player games, classify their computational complexity, and discuss strategy synthesis algorithms. We provide an encoding from the business processes we consider here into CCNDs to exploit off-the-shelf their strategy synthesis algorithms. We introduce $$\textsc {Zeta}$$ Z E T A , a tool for checking controllability of CCNDs, synthesizing execution strategies, and executing controllable CCNDs, by also supporting user interactivity. We use $$\textsc {Zeta}$$ Z E T A to compare with the previous research, provide a new experimental evaluation for CCNDs, and discuss limitations.

Download Full-text

How to model planning and scheduling problems using constraint networks on timelines

The Knowledge Engineering Review ◽

10.1017/s0269888910000172 ◽

2010 ◽

Vol 25 (3) ◽

pp. 319-336 ◽

Cited By ~ 13

Author(s):

Gérard Verfaillie ◽

Cédric Pralet ◽

Michel Lemaître

Keyword(s):

Dynamic Systems ◽

Discrete Event ◽

Discrete Event Dynamic Systems ◽

Scheduling Problems ◽

Planning And Scheduling ◽

Constraint Networks ◽

Modeling Power ◽

Mission Management ◽

Event Dynamic ◽

Domain Management

AbstractThe CNT framework (Constraint Network on Timelines) has been designed to model discrete event dynamic systems and the properties one knows, one wants to verify, or one wants to enforce on them. In this article, after a reminder about the CNT framework, we show its modeling power and its ability to support various modeling styles, coming from the planning, scheduling, and constraint programming communities. We do that by producing and comparing various models of two mission management problems in the aerospace domain: management of a team of unmanned air vehicles and of an Earth observing satellite.

Download Full-text

Temporal constraint networks

Artificial Intelligence ◽

10.1016/0004-3702(91)90006-6 ◽

1991 ◽

Vol 49 (1-3) ◽

pp. 61-95 ◽

Cited By ~ 794

Author(s):

Rina Dechter ◽

Itay Meiri ◽

Judea Pearl

Keyword(s):

Temporal Constraint ◽

Constraint Networks

Download Full-text

Tree Trimming: Four Non-Branching Rules for Priest’s Introduction to Non-Classical Logic

The Australasian Journal of Logic ◽

10.26686/ajl.v12i2.2066 ◽

2017 ◽

Vol 12 (2) ◽

Author(s):

Marilynn Johnson

Keyword(s):

Modal Logic ◽

Classical Logic ◽

Variable Domain ◽

Free Logic ◽

Intuitionist Logic ◽

Branching Rule ◽

Branching Rules ◽

Graham Priest

In An Introduction to Non-Classical Logic: From If to Is Graham Priest (2008) presents branching rules in Free Logic, Variable Domain Modal Logic, and Intuitionist Logic. I propose a simpler, non-branching rule to replace Priest’s rule for universal instantiation in Free Logic, a second, slightly modified version of this rule to replace Priest’s rule for universal instantiation in Variable Domain Modal Logic, and third and fourth rules, further modifying the second rule, to replace Priest’s branching universal and particular instantiation rules in Intuitionist Logic. In each of these logics the proposed rule leads to tableaux with fewer branches. In Intuitionist logic, the proposed rules allow for the resolution of a particular problem Priest grapples with throughout the chapter. In this paper, I demonstrate that the proposed rules can greatly simplify tableaux and argue that they should be used in place of the rules given by Priest.

Download Full-text

A variable-free logic for mass terms.

Notre Dame Journal of Formal Logic ◽

10.1305/ndjfl/1093634400 ◽

1992 ◽

Vol 33 (3) ◽

pp. 348-358 ◽

Cited By ~ 4

Author(s):

William C. Purdy

Keyword(s):

Free Logic ◽

Mass Terms

Download Full-text

On Robustness in Qualitative Constraint Networks

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2020/251 ◽

2020 ◽

Author(s):

Michael Sioutis ◽

Zhiguo Long ◽

Tomi Janhunen

Keyword(s):

Linear Space ◽

Job Shop ◽

Job Shop Scheduling ◽

Temporal Information ◽

Challenging Problem ◽

Constraint Networks ◽

Shop Scheduling ◽

Preliminary Results ◽

All Solutions

We introduce and study a notion of robustness in Qualitative Constraint Networks (QCNs), which are typically used to represent and reason about abstract spatial and temporal information. In particular, given a QCN, we are interested in obtaining a robust qualitative solution, or, a robust scenario of it, which is a satisfiable scenario that has a higher perturbation tolerance than any other, or, in other words, a satisfiable scenario that has more chances than any other to remain valid after it is altered. This challenging problem requires to consider the entire set of satisfiable scenarios of a QCN, whose size is usually exponential in the number of constraints of that QCN; however, we present a first algorithm that is able to compute a robust scenario of a QCN using linear space in the number of constraints. Preliminary results with a dataset from the job-shop scheduling domain, and a standard one, show the interest of our approach and highlight the fact that not all solutions are created equal.

Download Full-text