finite-time reachability of a class of discrete-time PWA systems over a class of polyhedra
The problem is as follows. Given a model, a set of initial conditions X(0) and a time horizon N, we want to compute the states reachable at time 1, 2, ..., N. In other words, we want to determine X(1), X(2), ..., X(N).
The model is a class of discrete-time PWA systems:
x(k+1) = A_i x(k) + b_i, if x(k) \in R_i where i \in {1,...,M}
For each i \in {1,...,M}, there is a single element in each row of matrix A_i with the value of 1 and the others are 0.
The region R_i for i \in {1,...,M} and the set of initial conditions is described as a class of polyhedra. This polyhedra is an intersection of sets of the following form: {x_i - x_j < const} or {x_i - x_j <= const}.
It sounds like it be an interesting case. Could you provide a concrete example that you think would be a good candidate for the tool competition?
Hi Dieky,
this sounds very interesting. I have a few questions:
1) What kind of specification would you like to check?
2) Where would such a system occur in practice? Please not that the goal of ARCH is to foster the technology transfer from academia to industry, so it is important that the benchmarks have concrete applications.
On the category: It's a piecewise affine system and it's a bounded model checking problem. The system can be embedded in a hybrid automaton with piecewise constant dynamics (Henzinger-LHA). So both HPWC and HBMC would make sense. HPWC is fine with me, but if you're using an approach that is built on bounded depth (e.g., SMT without induction), then HBMC might be a better fit. For example, if BACH can run this system, then HBMC would fit.
It would be great if you had an illustration of the kind of behavior (plots etc.).
Best wishes,
Goran
Dear Goran,
I would like to propose a safety verification problem over the max-plus model of ribosome dynamics during mRNA translation. The max-plus model has been discussed in:
https://doi.org/10.1016/j.jtbi.2012.03.007
In this model, x(k) represents the time instant of k-th ribosome leaves all codons. The safety verification problem over this model can be interpreted as follows. Suppose we know the time instant when the first ribosome leaves all codons. We would like to know whether after 100 time units, the 10th ribosome has left all codons.
Dear Dieky,
This looks interesting. Do I read it right that the big instance in the paper corresponds to a system with ~500 variables? Would you be able to provide some kind of automaton-like description?
Best wishes,
Goran
Dear Goran,
With respect to the model from systems biology I mentioned earlier, we face some difficulties in finding the parameter values. Thus, we will find another model, possibly related with transportation, because it is more understandable.
First of all, thanks for your positive response.
In this message, I have attached a pdf file that contains the model, the specification, and the application. The model represents a subset of Dutch railway network. The specification is a simple safety specification.
With regards to the category, I have to admit that I am not familiar with both HPWC and HBMC. Thus, I need your suggestion, which category is suitable for the problem.
Dieky
case_study.pdf