scholarly journals PCF-based formalization of the parallel composition of automata

2019 ◽  
Author(s):  
A. Davydov ◽  
A. Larionov ◽  
N. Nagul

The paper demonstrates how the automatic theorem proving technique of the PCF calculus is applied to construct parallel composition of automata. Parallel composition plays an essential role in the supervisory control theory at different stages of systems and supervisors design. Improved formalization of discrete event systems as positively-constructed formulas along with auxiliary predicates, serving for accessibility of the automaton checking, simplify parallel composition construction.

2014 ◽  
Vol 11 (4) ◽  
pp. 1229-1247 ◽  
Author(s):  
Eduardo Santos ◽  
Agnelo Vieira ◽  
Sauro Schaidt ◽  
Eduardo Loures

Constraint-based processes require a set of rules that limit their behavior to certain boundaries. In these processes, the control flow is defined implicitly as a set of constraints or rules, and all possibilities that do not violate any of the given constraints are allowed to be executed. The present paper proposes a new approach to deal with constraint-based processes. The proposed approach is based on Supervisory Control Theory, a formal foundation for building controllers for discrete-event systems. The controller proposed in this paper monitors and restricts execution sequences of activities such that constraints are always obeyed. We demonstrate that our approach may be used as a declarative language for constraint-based processes. In order to provide support for users of such processes and to facilitate the using of our control approach, we offer a set of constraints modeled by automata. This set encompasses the constraints frequently needed in workflow system.


Sign in / Sign up

Export Citation Format

Share Document