a particular kind of mathematically-based technique for the specification, development and verification of software and hardware systems.
1
vote
3answers
98 views
Binary decision diagram for a six-figure Boolean function
Let $p$ be the six-figure Boolean function with the following definition:
$p(x_{0},x_{1},x_{2},x_{3},x_{4},x_{5})=\begin{cases}
true & \text{if } x_{0}=x_{5} \text{ and } x_{1}=x_{4} ...
1
vote
0answers
53 views
Logical conjunction of two binary decision diagrams
Compute a BDD for $B_{1} \wedge B_{2}$ by using an algorithm that applies dynamic programming. Document the execution of the algorithm by indicating pairs of BDDs $(q_{1},q_{2})$ and the BDD $q_{1} ...
0
votes
1answer
86 views
Initial Algebra example
If the definition of Initial Algebra is:
"An object is initial if there exists a unique morphism from the object to every
object in the category"
Why do we need such object, and could any one give ...
2
votes
1answer
65 views
Reference Request for Synthesis
New to the world of software verification and synthesis. It was suggested to me that the book "Principles of Model Checking" is a good reference for verification, but I am clueless about synthesis. ...
5
votes
2answers
150 views
Introduction into first order logic verification
I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
4
votes
1answer
95 views
How to implement simulation on two LTSs?
Does any one know how to implement the simulation relation on two labelled transition systems (LTS)?
I know how to do it for branching bi-simulation. The signature refinement theorem is used for ...
3
votes
1answer
69 views
Looking for a book that derives and constructs a model checking application
I am teaching myself program verification and am currently learning proof assistants. I have the book Handbook of Practical Logic and Automated Reasoning which gives the proofs necessary for the ...
3
votes
1answer
103 views
Witness for the $EU(\phi_1,\phi_2)$ using BDDs
I wanted ask if you know an algorithm to find the witness for $EU(\phi_1,\phi_2)$ (CTL formula "Exist Until") using BDDs (Binary Decision Diagram). In pratice you should use the fixed point for ...
3
votes
1answer
65 views
Time to construct a GNBA for LTL formula
I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula:
Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ ...
9
votes
4answers
429 views
How do you check if two algorithms return the same result for any input?
How do you check if two algorithms (say, Merge sort and Naïve sort) return the same result for any input, when the set of all inputs is infinite?
Update: Thank you Ben for describing how this is ...
7
votes
2answers
411 views
A Question relating to a Turing Machine with a useless state
OK, so here is a question from a past test in my Theory of Computation class:
A useless state in a TM is one that is never entered on any input string. Let $$\mathrm{USELESS}_{\mathrm{TM}} = ...
5
votes
1answer
99 views
Late and Early Bisimulation
This is a follow up to my earlier questions on coinduction and bisimulation.
A relation $R \subseteq S \times S$ on the states of an LTS is a bisimulation iff $\forall (p,q)\in R,$
$$
...
9
votes
3answers
353 views
When are two simulations not a bisimulation?
Given a labelled transition system $(S,\Lambda,\to)$, where $S$ is a set of states, $\Lambda$ is a set of labels, and $\to\subseteq S\times\Lambda\times S$ is a ternary relation. As usual, write $p ...
24
votes
2answers
497 views
What is coinduction?
I've heard of (structural) induction. It allows you to build up finite structures from smaller ones and gives you proof principles for reasoning about such structures. The idea is clear enough.
...
10
votes
3answers
270 views
Path to formal methods
It is not uncommon to see students starting their PhDs with only a limited background in mathematics and the formal aspects of computer science. Obviously it will be very difficult for such students ...
8
votes
5answers
160 views
Is it possible to solve the halting problem if you have a constrained or a predictable input?
The halting problem cannot be solved in the general case. It is possible to come up with defined rules that restrict allowed inputs and can the halting problem be solved for that special case?
For ...
19
votes
2answers
322 views
Equivalence of Büchi automata and linear $\mu$-calculus
It's a known fact that every LTL formula can be expressed by a Büchi $\omega$-automaton. But, apparently, Büchi automata are a more powerful, expressive model. I've heard somewhere that Büchi automata ...
11
votes
6answers
394 views
Algorithm to solve Turing's “Halting problem”
"Alan Turing proved in 1936 that a general algorithm to solve the
halting problem for all possible program-input pairs cannot exist"
Can I find a general algorithm to solve the halting problem ...
