Protocol queries with Decision Nodes and time

[danbryce]

Decision nodes represent tests on protocol values that may arise at run time. The typical query we're supporting is the minimal duration of a protocol. With decision nodes, that means there are multiple execution paths of the protocol. In such cases, every descendant of a decision node is conditional (upon the outcome of the decision node). What should be the query for the protocol in this case?

My thought is that we should compute the duration of each possible execution path and then provide the set, or provide some statistics (e.g., min, max, mean, etc.).

Encoding and solving the problem is another issue. The brute force method could enumerate the combinations of branch conditions and solve for each. The next best thing might be to compute the possible execution paths using something like an ATMS (https://arxiv.org/pdf/1401.4606.pdf).