Priority scheduling of distributed systems based on model checking (Q453501): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(7 intermediate revisions by 6 users not shown) | |||
Property / author | |||
Property / author: Doron A. Peled / rank | |||
Property / author | |||
Property / author: Doron A. Peled / rank | |||
Normal rank | |||
Property / review text | |||
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. | |||
Property / review text: 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. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Pierre Leone / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68M14 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68M20 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q60 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q85 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6087620 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
model checking | |||
Property / zbMATH Keywords: model checking / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
Petri nets | |||
Property / zbMATH Keywords: Petri nets / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
synthesis | |||
Property / zbMATH Keywords: synthesis / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
controller design | |||
Property / zbMATH Keywords: controller design / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
knowledge | |||
Property / zbMATH Keywords: knowledge / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
temporal logic | |||
Property / zbMATH Keywords: temporal logic / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: CESAR / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/s10703-011-0128-y / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2134284203 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Priority Scheduling of Distributed Systems Based on Model Checking / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Methods for Knowledge Based Controlling of Distributed Systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3906386 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4845472 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: System modelling with high-level Petri nets / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Achieving distributed control through model checking / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A little knowledge goes a long way / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Common knowledge and update in finite environments / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Supervisory Control of a Class of Discrete Event Processes / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Know means no: Incorporating knowledge into discrete-event control systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Think globally, act locally: decentralized supervisory control / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Undecidability in decentralized supervision / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Undecidable problems of decentralized observation and control on regular languages / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A general architecture for decentralized supervisory control of discrete-event systems / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 18:08, 5 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Priority scheduling of distributed systems based on model checking |
scientific article |
Statements
Priority scheduling of distributed systems based on model checking (English)
0 references
27 September 2012
0 references
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.
0 references
model checking
0 references
Petri nets
0 references
synthesis
0 references
controller design
0 references
knowledge
0 references
temporal logic
0 references