基于顶点移除同步图积的两种图分解定理的修正

近来，我们基于一种新的图积（顶点移除同步积(VRSP)）引入了两种图分解定理，其动机源于同步周期实时过程的应用背景。在这些应用中，周期实时过程在具有相同标签因而具有相同行为的动作上同步。从进程代数角度看，此类同步动作由字母表中包含该动作的所有进程原子地、同时地执行。但当这些进程在某计算机平台上执行时，同步会导致进程的上下文切换，从而增加开销，并可能导致截止期限错过。而通过组合进程，我们减少了上下文切换次数，进而降低了开销。我们通过将进程表示为边标记无环有向多重图，并以VRSP对图作乘积来组合这些进程。接着，我们将所得图转置为具有更少上下文切换的进程。这些实时应用的一个重要方面是必须按时执行。尽管如此，仍可能发生应用进程集无法及时执行并错过截止期限的情况。此时，通过分解图并以另一种组合用VRSP对图作乘积，由这些重组图所表示的进程便可按时执行。近期引入的图分解定理要求过于严格，可予以放宽，从而使更多图可被分解，为实时应用提供更多可能组合。因此，我们回顾VRSP的定义及两种图分解定理，通过陈述并证明两个引理放宽要求，并借助这些引理陈述并证明这两种（放宽后的）图分解定理。