Свойства предикатного трансформера системы VRS

Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В...

Повний опис

Збережено в:
Бібліографічні деталі
Опубліковано в: :Кибернетика и системный анализ
Дата:2010
Автори: Летичевский, А.А., Годлевский, А.Б., Летичевский, А.А. (мл.), Потиенко, С.В., Песчаненко, В.С.
Формат: Стаття
Мова:Russian
Опубліковано: Інститут кібернетики ім. В.М. Глушкова НАН України 2010
Теми:
Онлайн доступ:https://nasplib.isofts.kiev.ua/handle/123456789/45239
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-45239
record_format dspace
spelling Летичевский, А.А.
Годлевский, А.Б.
Летичевский, А.А. (мл.)
Потиенко, С.В.
Песчаненко, В.С.
2013-06-10T16:10:12Z
2013-06-10T16:10:12Z
2010
Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос.
0023-1274
https://nasplib.isofts.kiev.ua/handle/123456789/45239
519.686.2
Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В постумовах базових протоколів використовуються оператори присвоювання, оновлення черг та довільні формули. Для здійснення переходу із одного стану в інший побудовано предикатний трансформер як функцію перетворення формул. Доведено основну властивість предикатного трансформера, згідно якій він обчислює найсильнішу постумову для символьних станів.
The paper considers models specified in basic protocol language. They are attribute transition systems and their states are defined by formulas of first-order multisort predicate calculus over system attributes. Attributes of simple numeric and symbolic types, functional types, and queues are allowed. Assignment operators, queue update operators, and arbitrary formulas are used in postconditions of basic protocols. To pass from one state to another, a predicate transformer has been set up as a function of formula transformation. The main property of the predicate transformer has been proved: it calculates the strongest postcondition for symbolic states.
ru
Інститут кібернетики ім. В.М. Глушкова НАН України
Кибернетика и системный анализ
Кибернетика
Свойства предикатного трансформера системы VRS
Властивості предикатного трансформера системи VRS
Properties of a predicate transformer of VRS system
Article
published earlier
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title Свойства предикатного трансформера системы VRS
spellingShingle Свойства предикатного трансформера системы VRS
Летичевский, А.А.
Годлевский, А.Б.
Летичевский, А.А. (мл.)
Потиенко, С.В.
Песчаненко, В.С.
Кибернетика
title_short Свойства предикатного трансформера системы VRS
title_full Свойства предикатного трансформера системы VRS
title_fullStr Свойства предикатного трансформера системы VRS
title_full_unstemmed Свойства предикатного трансформера системы VRS
title_sort свойства предикатного трансформера системы vrs
author Летичевский, А.А.
Годлевский, А.Б.
Летичевский, А.А. (мл.)
Потиенко, С.В.
Песчаненко, В.С.
author_facet Летичевский, А.А.
Годлевский, А.Б.
Летичевский, А.А. (мл.)
Потиенко, С.В.
Песчаненко, В.С.
topic Кибернетика
topic_facet Кибернетика
publishDate 2010
language Russian
container_title Кибернетика и системный анализ
publisher Інститут кібернетики ім. В.М. Глушкова НАН України
format Article
title_alt Властивості предикатного трансформера системи VRS
Properties of a predicate transformer of VRS system
description Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В постумовах базових протоколів використовуються оператори присвоювання, оновлення черг та довільні формули. Для здійснення переходу із одного стану в інший побудовано предикатний трансформер як функцію перетворення формул. Доведено основну властивість предикатного трансформера, згідно якій він обчислює найсильнішу постумову для символьних станів. The paper considers models specified in basic protocol language. They are attribute transition systems and their states are defined by formulas of first-order multisort predicate calculus over system attributes. Attributes of simple numeric and symbolic types, functional types, and queues are allowed. Assignment operators, queue update operators, and arbitrary formulas are used in postconditions of basic protocols. To pass from one state to another, a predicate transformer has been set up as a function of formula transformation. The main property of the predicate transformer has been proved: it calculates the strongest postcondition for symbolic states.
issn 0023-1274
url https://nasplib.isofts.kiev.ua/handle/123456789/45239
citation_txt Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос.
work_keys_str_mv AT letičevskiiaa svoistvapredikatnogotransformerasistemyvrs
AT godlevskiiab svoistvapredikatnogotransformerasistemyvrs
AT letičevskiiaaml svoistvapredikatnogotransformerasistemyvrs
AT potienkosv svoistvapredikatnogotransformerasistemyvrs
AT pesčanenkovs svoistvapredikatnogotransformerasistemyvrs
AT letičevskiiaa vlastivostípredikatnogotransformerasistemivrs
AT godlevskiiab vlastivostípredikatnogotransformerasistemivrs
AT letičevskiiaaml vlastivostípredikatnogotransformerasistemivrs
AT potienkosv vlastivostípredikatnogotransformerasistemivrs
AT pesčanenkovs vlastivostípredikatnogotransformerasistemivrs
AT letičevskiiaa propertiesofapredicatetransformerofvrssystem
AT godlevskiiab propertiesofapredicatetransformerofvrssystem
AT letičevskiiaaml propertiesofapredicatetransformerofvrssystem
AT potienkosv propertiesofapredicatetransformerofvrssystem
AT pesčanenkovs propertiesofapredicatetransformerofvrssystem
first_indexed 2025-12-07T13:14:25Z
last_indexed 2025-12-07T13:14:25Z
_version_ 1850855407878144000