Priority scheduling of distributed systems based on model checking
Distributed systems (68M14) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
One can imagine the design of concurrent systems in two stages. The first one consists in the description of the behaviour of the isolated processes while the second one consists in the definition of the inter-processes synchronization, i.e., the rules that lead to the activation or deactivation of a process depending on the current states of the other processes that compose the system. However, a further constraint must be added to make this design methodology realistic. Namely, the activation/deactivation of the processes need to result from local knowledge of the system. This is an issue since very often the synchronization expresses a global constraint. In this article, the authors address this issue in the framework of Petri nets with priorities. Priorities are defined by a partial order relation among the transitions of the Petri nets. An enabled transition can be fired only if there is no higher priority transition that is also enabled. The issue that is addressed is how transforming a prioritized Petri net \(P\) to a classical Petri net \(P'\) that implements the priority of \(P\). Moreover, \(P'\) makes use of local information. The method that is proposed in this article is based on formal methods of model checking that make possible to identify the situations where local information is sufficient to implement priorities.
- A general architecture for decentralized supervisory control of discrete-event systems
- A little knowledge goes a long way
- Achieving distributed control through model checking
- Common knowledge and update in finite environments
- scientific article; zbMATH DE number 3714896 (Why is no real title available?)
- scientific article; zbMATH DE number 795590 (Why is no real title available?)
- Know means no: Incorporating knowledge into discrete-event control systems
- Methods for knowledge based controlling of distributed systems
- Priority Scheduling of Distributed Systems Based on Model Checking
- Supervisory Control of a Class of Discrete Event Processes
- System modelling with high-level Petri nets
- Think globally, act locally: decentralized supervisory control
- Undecidability in decentralized supervision
- Undecidable problems of decentralized observation and control on regular languages
- Systems with priorities: conformance, testing, and composition
- Knowledge based scheduling of distributed systems
- Priority Scheduling of Distributed Systems Based on Model Checking
- scientific article; zbMATH DE number 1293734 (Why is no real title available?)
- Building distributed controllers for systems with priorities
- Liveness enforcement for production systems modeled by time Petri nets
This page was built for publication: Priority scheduling of distributed systems based on model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q453501)
