Abstract
We consider logics which define different properties of functions – such as injectivity, surjectivity, monotonicity, etc. – in the context of temporal×modal logic. In this type of logics, the possible worlds semantics is modified by considering each world as a temporal flow and using accessibility functions to represent the connection among them. This approach is adequate to model interactions between processes with clocks that can be either synchronized or not. We study the definability and give indexed axiomatic systems for these properties.
Acknowledgements
Partially supported by the Spanish research projects TIN2006-15455-C03-01 and P6-FQM-02049.