Рассмотрено применение ТSS-алгоритма построения минимального порождающего множества решений системы линейных диофантовых уравнений к анализу сетей Петри. В частности, с помощью этого алгоритма строятся минимальные множества инвариантов сетей Петри.

Наведено достатні критерії еквівалентності ймовірнісних мір, що відповідають гаусівським однорідним випадковим полям, в термінах спектральних щільностей полів, що розглянуто. Зазначені критерії надано у формі, що враховує можливість обертання у нуль вказаних спектральних щільностей.

Наведено огляд декількох сучасних алгоритмів розв'язку систем лінійних діофантових рівнянь в області натуральних чисел, а також описується інкрементальна версія методу перевірки на сумісність систем таких рівнянь і нерівностей.

Індекс рубрикатора НБУВ: В142.2

Рубрики:

Діофантові рівняння. Невизначені рівняння

Шифр НБУВ: Ж16833 Пошук видання у каталогах НБУВ 

Розглянуто два алгоритми розв'язку систем лінійних діофантових констрейнтів у множині {0,1}. Досліджено деякі властивості даних алгоритмів щодо оцінки їх складності.

Описано програмну реалізацію алгоритму перетворення неординарної мережі Петрі в ординарну. В основу програми покладено алгоритм, запропонований Хаком. Алгоритм реалізовано в програмному забезпеченні "Перетворювач мереж Петрі", створеному на мові програмування C++Builder.

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

Представлено загальний огляд застосувань формальних методів для специфікації та верифікації програмних технічних систем, а також запропоновано підхід до ідентифікації розв'язку проблеми конфлікту функціональностей (Feature Interaction) у телекомунікаційних системах за допомогою формальних методів.

Приведен краткий обзор использования формальных методов в области спецификации и верификации, где основное внимание уделено методам проверки на модели (model checking) и доказателей теорем (theorem proving). Обсуждены другие возможные направления и фундаментальные концепции в области интеграции различных методов, технологические и технические трудности при применении формальных методов.

Ключ. слова: реактивные алгоритмы, спецификация, язык L, выполнимость формулы, глубина формулы, множество конъюнктов
Індекс рубрикатора НБУВ: З973-018

Рубрики:

Комп'ютери та програмування

Шифр НБУВ: Ж29144 Пошук видання у каталогах НБУВ 

Запропоновано поліноміальні алгоритми побудови базису множини розв'язків системи лінійних однорідних і неоднорідних діофантових рівнянь в кільці лишків за модулем деякого числа за умови відомого розкладу модуля на прості множники.

Запропоновано поліноміальні алгоритми побудови базису множини розв'язків системи лінійних однорідних і неоднорідних діофантових рівнянь в полі лишків за модулем простого числа.

Розглянуто методи розв'язання систем лінійних однорідних діофантових рівнянь в множині натуральних чисел та в множині {0, 1}. Наведено відповідні алгоритми, їх властивості і оцінки часової складності.

Ключ. слова: язык L, выполнимость формулы, глубина формулы, множество конъюнктов, представление данных, оценка сложности
Індекс рубрикатора НБУВ: З973-018.2

Рубрики:

Комп'ютери та програмування

Шифр НБУВ: Ж29144 Пошук видання у каталогах НБУВ 

Описан подход к проверке противоречивости множества дизъюнктов в исчислении высказываний методом резолюций, основанный на модифицированном TSS-методе решения систем линейных однородных диофантовых уравнений.

Описан алгоритм перевода документа MSC в трассово эквивалентную ему сеть Петри. Полученную таким образом сеть Петри можно использовать для анализа свойств системы, представленной исходным документом MSC. Алгоритм является частью инструментария для автоматического анализа и верификации документов MSC.

Індекс рубрикатора НБУВ: В142.2

Рубрики:

Діофантові рівняння. Невизначені рівняння

Шифр НБУВ: Ж29144 Пошук видання у каталогах НБУВ 

Розглянуто остаточний варіант алгоритму трансляції документів з мови MSC-2000 у мережі Петрі, що подійно еквівалентні до них. Вхідний документ може використовувати довільні елементи мови MSC-2000, але значення елементів у мовах не використовується; послідовна композиція діаграм інтерпретується як строга. Наведений алгоритм реалізовано як повнофункціональний прототип, що може використовуватися для верифікації програмних систем.

Описано реалізацію алгоритму переведення набору діаграм MSC (документа MSC) в подійно еквівалентну йому мережу Петрі, наведено доказ коректності зазначеного алгоритму. Мережа, що одержана таким чином, може використовуватися для аналізу властивостей вихідного документа MSC. Наведений алгоритм є складовою частиною системи аналізу та верифікації документів MSC.

Рассмотрены методы и принципы онтологического подхода к построению и проектированию знание-ориентированных информационных систем с онтолого-управляемой архитектурой, реализующих технологию извлечения предметно-ориентированных знаний из множества естественно-языковых текстов, их формально-логического представления и прикладной обработки. Изложены методики проектирования таких систем и компьютерных онтологий произвольных предметных областей, рассмотрены принципы и алгоритмы функционирования инструментального комплекса автоматизированого проектирования компьютерных онтологий. Приведены примеры построения онтологической системы для заданной предметной области и реализации некоторых процедур Text processing & mining. Предложены алгебра и система списочных структур, формализующие процесс обработки текстовой информации.