Questions tagged [transition-systems]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0
votes
1answer
17 views

Stratification of Bisimilarity : $\sim$ does not coincide with $\sim_\omega$

I am reading Sangiorgi's paper On the origins of bisimulation an coinduction. Definition 2.5, on page 5, defines Stratification of Bisimilarity: Let $W$ be the states of an LTS. We set: $\sim_0 \...
0
votes
0answers
8 views

Environmental/Economical benefits of not transmitting parts of a video?

Are there any potential environmental och economical benefits (in terms of infrastructure) derived from not transmitting video packets unless absolutely necessary or requested by the client for Media-...
0
votes
0answers
27 views

How to deal with sets in NFA?

I have a transition system that I'm converting to an NFA. In the TS, I have a trace of {b} {a, b} {a, b, c}. How would I handle these sets in the NFA? In other words, what would be the path to follow ...
1
vote
0answers
86 views

Bisimulation, bisimulation equivalence and simulation equivalence?

I got a little confused with these 3 concepts. Is there a difference between bisimulation and bisimulation equivalence and if yes, then what is it? Also, if we say that the LTS's X and Y are bisimilar,...
2
votes
1answer
84 views

Restriction and re-labeling on CCS

In a process like $$ R \stackrel{def}=((a.\bar{b}.0)\setminus\{b\})[a\to b]\mid(\bar{b}.b.0)+\bar{b}.c.0 $$ $b$ is restricted to perform on the inner process of RHS $(a.\bar{b}.0)\setminus\{b\}$, ...
0
votes
1answer
47 views

State Machine and State transition Table - Explanation and Creation Of

How do I create a state transition table/array in actual code/pseudo-code? I haven't experienced the "ah-ha" moment yet with the state machine to coding (and I really want to). I've looked at several ...
1
vote
1answer
91 views

CCS synchronization

Within CSS we talk about binary interactions. Does this prevent synchronizing multiple processes in one step? Example: $P_1 ::= a.D$ $P_2 ::= \overline{a}.D$ $P_3 ::= a.D$ Let's consider the ...
2
votes
1answer
389 views

Modeling a sequential circuit as a transition system

I was asked to model the following sequential circuits C1, C2 as transition systems (i.e. identify the output y function and register functions r1, r2, r3) For C2 there appears to be not input x and ...
2
votes
0answers
149 views

Proving weak simulation

I want to prove something but I am not sure if it is the right way to do it. I have two LTS that define different semantics. A=($Q_a,Λ,\to)$, and B=$(Q_b,Λ\cup\{\beta\},\leadsto)$, where $\beta$ is ...
2
votes
1answer
596 views

The Interleaved Transition System for 2 Independent and Concurrent Transition Systems

This question is about Model Checking for Software Formal Verification How do you model the joint behavior of 2 independent and concurrent transition systems? Specifically, given the two independent ...
6
votes
4answers
2k views

What is the difference (if any) between transition systems and finite automata?

is there any difference between transition systems and finite automata? Is it that transition systems consist of both NFA (nondeterministic finite automata) and DFA (deterministic finite automata)?
1
vote
0answers
85 views

Example of Zeno timed automaton

Is there an example of a timed automaton that requires infinite clock precision, in order to be controller so as to avoid a deadlock or bad state? I.e. a transition system that consists of nodes ...
2
votes
0answers
37 views

How to prove that justice isn't enough to produce all naturals?

I'm doing the exercises from the first chapter of the book "Temporal Verification of Reactive Systems Safety" by Manna and Pnueli. However I find very difficult to solve the point c of problem 0.2. ...
3
votes
1answer
771 views

Modelling a basic sequential circuit as a transition system?

I'm going through Dr Joost-Pieter Katoen's slides and stumbled upon this: For some reason I can't quite make out how the transition system relates to the sequential circuit. If I had a question for ...
0
votes
1answer
191 views

Applying DFS algorithm to a transition system to find reachable states

Currently working on a past exam question which tells me to compute the product of two transition systems and then use DFS to find the reachable states of the product. I learnt how to compute the ...
2
votes
1answer
2k views

What is the difference between a Transition System and a Program Graph? (model checking) [closed]

As the above question says. I'm wondering if a transition system is the same as a program graph or they are two different things? Thank you.