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

learn more… | top users | synonyms

6
votes
0answers
29 views

Boolean formula that agrees with most truth assignments

Let $X_1,\dots,X_n$ be $n$ boolean variables. I have an unknown predicate $P(X_1,\dots,X_n)$ on these boolean variables. Of course, I can view the predicate as a function $f_P : \{0,1\}^n \to ...
2
votes
0answers
35 views

Is there any open-source tools for verifying TCTL formulae over timed automata can be imported into my project?

In my project, there is one important step to automatically verify a timed automata with TCTL formulae. I briefly surveyed the tool UPPAAL that provides a GUI to construct a timed automata and to ...
1
vote
0answers
133 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} ...