Недетерминированные автоматы в проектировании систем параллельной обработки. Вашкевич Н.П. - 83 стр.

                                 j k1
           S i , (t )  V (τ) i ,,j  (τ) & ( τ1 )e( τ1 ) & S i,,j1 ( τ  1) 
                                 j 1 t                1 t
                                                                                                                 (4.47)
                         j k2
                        V   (τ) i,,k  j  (τ) & ( τ1 )e( τ1 ) & S i , ( τ  1).
                                                 1

                         j 1 t                         t
                                                          1

где ,  - предикат формализующий частный входной сигнал.
       На основании аксиом, формализующих закон нейтральности пустого
слова (4.44), (4.45), нетрудно доказать, что выражение (4.47) в расширенном
исчислении предикатов эквивалентно выражению:
                                  j  k1
            S i , (t )    V (τ) i ,,j  (τ) & ( τ1 )qi , ( τ1 ) & S i,,j1 (τ  1) ,              (4.48)
                                  j 1 t                1 t
                          r k2
где   q i ,   τ1   V i ,,k  r  τ1  .
                                             1

                           r 1

       На основании изложенного при формализации словесных алгоритмов
функционирования цифровых автоматов можно использовать систему  A p ,
построенную на основе предикатных выражений вида (4.48), каждое из
которых представляет событие, реализуемое в автомате. При этом описания
таких событий имеют одинаковую структуру, состоящую из упомянутых
ранее трех частей (4.24): описание наступления события и его сохранения, и
описание непосредственно предшествующего события.

     4.2.3. Построение системы канонических уравнений по
описанию алгоритма обработки информации, представленным
на языке исчисления предикатов
      Система канонических уравнений, являющаяся основой для
построения структуры цифровых устройств обработки информации,
функционирование которых представлено на начальном языке исчисления
предикатов первого порядка, может быть получена из системы  A p как
способом, изложенным в [34], так и на основании аксиом (4.44) и (4.45).
      На основании аксиом (4.44) и (4.45) выражение вида (4.48)
преобразуется в каноническое уравнение по следующему алгоритму [37].
            1. Применить один раз аксиому 2 (4.45) к предикату ( τ1 )qi , ( τ1 )
                                                                                                       1 t
выражения (4.48). В результате чего получим:
                                    j  k1
                  S i , (t )  V (τ) i ,,j  (τ) & ( τ1 )e( τ1 ) & S i,,j1 ( τ  1) 
                                     j 1 t              1 t
                                                                                                                 (4.49)
         j  k1
       V (τ) i ,,j  (τ) & τ  t & qi , (t ) & ( τ1 )qi , ( τ1 ) & S i ,1 ( τ  1)
          j 1 t                                                   1 t



                                                                                                                          83