Modeling and Analysis of Three Properties of Mobile Interactive Systems Based on Variable Petri Nets.