a particular kind of mathematically-based technique for the specification, development and verification of software and hardware systems.

learn more… | top users | synonyms

11
votes
6answers
636 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 ...
27
votes
2answers
892 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. ...
12
votes
3answers
393 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 ...
20
votes
2answers
441 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 ...
10
votes
3answers
616 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 ...
9
votes
5answers
236 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 ...
1
vote
0answers
132 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} ...