English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Preemption is useful technique in real-time systems and several extensions of Merlin’s time Petri net have been proposed to model the preemption. However, in timed Petri nets, the modeling of the preemption has not been studied. On the other hand, by optimization of a SAT/SMT solver, large scale problems are solvable in a realistic computation time by using a SAT/SMT formulation. In this paper, first, we define preemptive controlled timed Petri nets abbreviated as pCTdPNs, where the control of the preemption is done by external input places. Next, we represent their dynamics using SMT formulae. Finally, we apply pCTdPNs to modeling of distributed mediators with several tasks executed by multi-processor systems, and obtain a task assignment to each processor and task scheduling using an SMT solver.

SMT Formulae of Preemptive Controlled Timed Petri Nets and its Application to Distributed Mediators