Jan Friso Groote

mCRL2 is a specification language for the behaviour of processes. Using the mCRL2 tools such behaviour can be analysed. The language contains abstractly specified datatypes such as (unbounded) natural numbers, integers, functions and (infinite) sets. We want to extend the language with real numbers, and common operations on these numbers. For this we believe that a variant of continued fractions would be suitable. Using matrix and tensor manipulation, operations such as addition and multiplication can be defined. Using infinite vector and matrix multiplication functions such as exp, log, sin etc. can be defined. However, convergence of infinite matrix multiplication, and with that its well definedness, is an issue that I have not solved and for which I seek advice. |