Notes on "Distributed reactive systems are hard to synthesize"

The original theorem of undecidability of distributed reactive systems appears in  Distributed reactive systems are hard to synthesize. Here I'd like to share some thoughts on the proof sketch presented in the the paper.

Two Flavours of Bounding in Bounded LTL Synthesis

Definitions and context is taken mainly from SF07.

There are two ways to "bound" in bounded synthesis approaches [KV05, SF07, FJR09]. The first one is to bound the size of the module synthesized. The second is to bound the number of visits to a bad state along the run path in the specification graph (informally can be seen as bounding the "reaction time" of the system) (here we count visits to different bad states separately).

Here are the differences:
1. Bounding |Impl| implies bounding |#bad_state_visits|:

|#bad_state_visits| <= |Impl|

2. .. but bounding bounding |#bad_state_visits| does not imply the bound on the implementation |Impl|!

The (2) can be easily seen in the specification: 

G(r -> Fg) & G(x <-> Xy & XXy & ..)

Bounding |#bad_state_visits| does not restrict the size of the implementation which depends on the specification -- the size essentially depends on how many X's we have in the second conjunct, and not on |#bad_state_visits|.

The (1) becomes clear if consider a run graph and a lasso with a bad state inside. The length of the lasso is equal to |bad SCC| * |Impl|. This lasso by definition contains all different pair of states (s_of_impl, s_of_graph), and it starts and closes in the same pair. Therefore the maximum number of visits to the bad state is achieved when all s_of_graph in the lasso are the same and equal to that bad state. Therefore, |#bad_state_visits| is bounded by |Impl|.

It is interesting to see other ways of boundings!

ltl2ba/ltl3ba fun optimization

These two equivalent formulae results in different automatae:
true -> (G(tok0 -> Fsends0) && GFg0) (1)
(G(tok0 -> Fsends0) && GFg0) (2)

..and corresponding automaton for the formula (1) (4 states):

..and the automaton for formula (2) contains 5 states, one more than previous:

..hacky way to optimize your automaton..

Синтез автоматов из LTL спецификаций

Начиная с января 2012 занимаюсь синтезом hardware из LTL спецификаций в TU Graz.

На вход принимается описание схемы в виде linear temporal logic (LTL). LTL содержит стандартные логические операторы and/or/not и временные операторы Globally/Future/Until. Благодаря этому можно описывать "временные" свойства системы. Например, формула G(r -> Fg)описывает простой арбитер и означает "Gлобально(в любой момент времени), если наблюдаем на входе сигнал r(request), то в будущем (in the Future), необходимо поднять сигнал g(grant)".

Из этой спецификации синтезируется автомат Мура (можно и Мили).

В кратце, это и есть проблема синтеза реактивной системы. Реактивная система - не очень хорошее название, более правильно сказать реагирующая система, система, которая постоянно находится во взаимодействии с окружением и никогда не останавливается. Это отличает её от "data crunch" систем, которые поглощают input data, обрабатывают её , выдают ответ и останавливаются. Примером реактивной системы может быть сотовый телефон, банкомат, сосед по парте.

Формально проблема синтеза выглядит так:

вход: LTL спецификация, разделение переменных на input/output

выход: автомат, либо "нет", если спецификация противоречивая

Проблема не новая. Первые работы - в 60х годах. Например, вот эта работа цитируется практически всеми - On the synthesis of a reactive module (1989). Сложность однако заключается в нижней вычислительной сложности синтеза - 2EXPTIME (double exponential) относительно размера спецификации. Как результат - малопрактично и мало внимания уделялось.  Исследователи подходили с разных сторон к облегчению проблемы - ограничивали язык спецификации, например (GR1 synthesis). Другой подход - это ограничить вид синтезируемых автоматов. Например, можно рассматривать только автоматы малого размера. Это важно с практической точки зрения - инженеров может не интересовать автомат, который хотя и отвечает спецификации, зато имеет 10000 состояний.

Где то в 2005 году и началось второе рождение этой области. Ключевая статья - Safraless decision procedures.

Сейчас мы используем для синтеза bounded synthesis метод, который позволяет задать лимит на размер синтезируемого автомата. Внутри, метод  сначала конвертирует LTL спецификацию в Universal coBuchi Automaton, затем в SMT query, который отправляется в SMT solver Z3 (по сути, проблема синтеза конвертируется в проблему SAT).

Мы сейчас работаем над близкой, но несколько иной проблемой - проблемой параметризованного синтеза (Parameterized Synthesis). Проблема совсем новая.

Проблема параметризованного синтеза выросла естественно из обычного синтеза. Схемы, которые пытались и пытаются синтезировать часто представляют собой разного рода арбитры, контроллеры, которые контроллируют доступ клиентов к некому ресурсу. Например, AMBA bus arbiter. Спецификация этого арбитра описывает доступ к общей шине нескольких клиентов. Клиент может запросить доступ к шине, получить доступ, переслать данные по шине, освободить шину, итд. Необходимо уметь синтезировать подобный арбитр. Но для скольких клиентов? Можно синтезировать разные арбитры для 2-3-4.. клиентов. Но возникает проблема - чем больше клиентов, тем сложнее задача.

На картинке вверху - время синтеза простого и посложнее арбитров в зависимости от числа клиентов. Зеленая штриховая линия - это время которое понадобилось бы, если бы не следующая идея.

Идея параметризованного синтеза простая - можно ли синтезировать базовый блок, который можно размножать и соединять друг с другом, масштабируя систему? Для некоторых спецификаций это можно. Например, это работает для простого арбитра со следующей спецификацией:

forall(i)        G(r_i -> Fg_i)
forall(i != j)   G(! (g_i & g_j))

Т.е. каждый request в конечном итоге обслужен, но невозможно одновременное предоставление гранта двум клиентам. Здесь, не задано конкретное число клиентов.

Для решения проблемы параметризованного синтеза мы используем интересный "cut-off" результат. Если рассматривать блоки организованные в token-rings, то для некоторых видов спецификаций достаточно синтезировать token-ring размера 4. Если удается синтезировать token ring такого размера, то из него можно вытащить базовый блок. Базовый блок затем можно соединять в token-rings любого размера.

Будущие направления:

• применить другие cut-off результаты
• cut-off independence: проверять, возможно ли масштабирование синтезированной схемы для случаев, для которых нет cut-off результатов
• ускорять синтез - процесс страшно медленный (сейчас удается синтезировать базовый блок из 4ех состояний за разумное время, этого мало)

Пара ссылок:
презентация на alpine verification meeting
основная статья, в которой была представлена проблема - Parameterized Synthesis

Python: ImportError: No module named

Problem
Traceback (most recent call last):
  File "model2graph.py", line 5, in <module>
    from mycore.extractor import extract
ImportError: No module named mycore.extractor

Solution

1. Always put __init__.py into directories of your Python project. If you want them to be treated as packages, of course.
2. Modify PYTHONPATH to include a current directory into Python packages search paths

Compiling Z3 programs on Ubuntu 11.04

I was getting some errors while trying to compile program that uses Z3 on Ubuntu 11.04.

/usr/include/c++/4.5/bits/locale_facets.h: In member function ‘iter_type std::num_get<_CharT, _InIter>::get(iter_type, iter_type, std::ios_base&, std::ios_base::iostate&, bool&) const’:

/usr/include/c++/4.5/bits/locale_facets.h:1958:33: error: expected primary-expression before ‘,’ token

The reason: __out and __in definitions in z3.h, z3_api.h interfere with variable names in c++locale.h and other system files.

To solve the problem undefine macroses difined in z3.h file, just add to the end of file:

#undef __in
#undef __out
#undef __inout
#undef __in_z
#undef __out_z
#undef __ecount
#undef __in_ecount
#undef __out_ecount
#undef __inout_ecount

Thanks to this post: http://sourceforge.net/projects/mingw-w64/forums/forum/723798/topic/3906648

git: how to push local branch to remote with a different name

git push remote_name local_branch_name:remote_branch_name
Thanks to http://markmcb.com/2008/09/21/multiple-remote-git-branches-with-different-local-names/
Use -n option for dry-run start to check that this works.