Skip to main content

Questions tagged [transition-systems]

2 votes
2 answers
104 views

Equivalence checking: product program vs bisimulation

Consider the problem of equivalence checking two terminating sequential programs $P$ and $P'$ with the same input signatures and return statements. Two programs are equivalent if for all inputs ($args$...
Albi's user avatar
  • 23
1 vote
1 answer
63 views

Reachable States in a Product of Transition Systems

I am trying to deepen my understanding of transition systems and synchronization schemes and would appreciate some insights. Consider the following scenario: We have three transition systems A1, A2, ...
Ahd 's user avatar
  • 11
0 votes
0 answers
46 views

ROBDDs heuristics for optimal variable ordering

I have this slide about how a BDD can vary in size depending on the order of the boolean variables fixed for it, and how it is NP-Complete to find the optimal ordering. It says there are heuristics ...
revision's user avatar
1 vote
1 answer
91 views

LTL Model Checking Worst Case size for NBA

I have a slide that gives the worst case time complexity of LTL model checking which uses a product construction of an LTS along with the NBA for the negation of the LTL formula. My question is, when ...
revision's user avatar
0 votes
2 answers
98 views

Irregular Safety Properties

A regular safety property is a safety property whose bad prefixes form a regular language, https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec4.pdf. My questions is, are there ...
revision's user avatar
2 votes
1 answer
173 views

Can CTL* express every model's behaviour

CTL* as in https://en.wikipedia.org/wiki/CTL*, is a logic that combines CTL and LTL. I know that CTL* can express everything expressible in these two languages and more. My question is whether we can ...
revision's user avatar
0 votes
1 answer
187 views

How does a Turing machine read a transition table as a function?

I am learning about Turing machines. I understand the alphabet set of symbols and the states a machine can be in. However, I do not understand how the transition function works. I come from a maths ...
Eris's user avatar
  • 13
0 votes
1 answer
620 views

Extended transition function in NFA

The following statement seems trivial, but how can it be formally proven/argued? $$\bigcup_{s \in \delta_{N}^{*}\left(q_{0}, w\right)} \delta_{N}^{*}(s, a) \;\equiv\; \delta_{N}^{*}\left(q_{0}, w a\...
Ronald's user avatar
  • 101
0 votes
1 answer
354 views

Transition System vs State Machines

Why there is no final state for a transition system? And why do NFA and DFA have final states? The transition system may or may not have any terminal states, but NFA/DFA has at least one final state (...
Jahid Chowdhury Choton's user avatar
2 votes
0 answers
75 views

Definition of nondeterministic transition system in Principles of Model Checking

In Sec 2.1 of Principles of Model Checking, by Christel Baier and Joost-Pieter Katoen, the authors talk about what constitutes a deterministic transition system (T.S.), and mention two kinds - action-...
Motorhead's user avatar
  • 301
1 vote
1 answer
142 views

When is a stuck state not final and when is a maximal sequence not complete in transition systems?

Reading the book Practical Foundations for Programming Language. In section 5.1 Transition Systems, the author said that Whereas all final states are, by convention, stuck, there may be stuck states ...
chansey's user avatar
  • 295
1 vote
0 answers
32 views

Has the similarity relation of a tree-shaped labelled transition system have finite index?

Let $T$ be an infinite countable labelled transition system with the shape of a tree and let $\sim$ be its similarity relation among nodes. Note that the alphabet of the labels is finite (hence the ...
Nicola Gigante's user avatar
0 votes
1 answer
203 views

For Turing machines, if the input variables increase, will the state set Q increase ? will the tape alphabet Γ increase?

For Turing machines, if the input variables increase, will the state set Q increase ? will the tape alphabet Γ increase? For example, for the SAT problem, the first question is whether the Boolean ...
lz9866's user avatar
  • 317
-2 votes
2 answers
1k views

Drawing transition diagram from transition table

I have a DFA transition table like \begin{array}{cc|c|c} & & 0 & 1 \\ \hline \to & p & qs & q \\ * & q ...
Manjoy Das's user avatar
1 vote
2 answers
4k views

NFA designing for strings starting with $01$

The question was asked Construct an NFA with set of all strings that start with $10$. The solution provided to me is But my question is what if the automaton receives an input $0$ at the starting? ...
Manjoy Das's user avatar

15 30 50 per page