This Article 
 Bibliographic References 
 Add to: 
Linear and Branching System Metrics
March/April 2009 (vol. 35 no. 2)
pp. 1-1
We extend the classical system relations of trace inclusion, trace equivalence, simulation, and bisimulation to a quantitative setting in which propositions are interpreted not as boolean values, but as elements of arbitrary metric spaces. Trace inclusion and equivalence give rise to asymmetrical and symmetrical linear distances, while simulation and bisimulation give rise to asymmetrical and symmetrical branching distances. We study the relationships among these distances and we provide a full logical characterization of the distances in terms of quantitative versions of LTL and mu-calculus. We show that, while trace inclusion (respectively, equivalence) coincides with simulation (respectively, bisimulation) for deterministic boolean transition systems, linear and branching distances do not coincide for deterministic metric transition systems. Finally, we provide algorithms for computing the distances over finite systems, together with a matching lower complexity bound.

[1] M.C. Browne, E.M. Clarke, and O. Grumberg, “Characterizing Finite Kripke Structures in Propositional Temporal Logic,” Theoretical Computer Science, vol. 59, pp.115-131, 1988.
[2] P. Caspi and A. Benveniste, “Toward an Approximation Theory for Computerized Control,” Proc. Second Int'l Workshop Embedded Software, pp.294-304, 2002.
[3] L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, and M. Stoelinga, “Model Checking Discounted Temporal Properties,” Theoretical Computer Science, vol. 345, pp.139-170, 2005.
[4] L. de Alfaro, T.A. Henzinger, and R. Majumdar, “Discounting the Future in Systems Theory,” Proc. 30th Int'l Colloquium Automated Language Progrogramming, pp.1022-1037, 2003.
[5] L. de Alfaro and R. Majumdar, “Quantitative Solution of Omega-Regular Games,” Proc. 33rd ACM Symp. Theory of Computing, pp.675-683, 2001.
[6] L. de Alfaro, R. Majumdar, V. Raman, and M. Stoelinga, “Game Relations and Metrics,” Proc. 22nd Ann. IEEE Symp. Logic in Computer Science, pp.99-108, 2007.
[7] C. Derman, Finite State Markovian Decision Processes. Academic Press, 1970.
[8] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, “Metrics for Labelled Markov Systems,” Proc. Concurrency Theory 10th Int'l Conf., pp.258-273, 1999.
[9] J. Filar and K. Vrieze, Competitive Markov Decision Processes. Springer-Verlag, 1997.
[10] P. Fletcher and W.F. Lindgren, Quasi-Uniform Spaces. Marcel Dekker, Inc., 1982.
[11] M. Huth and M. Kwiatkowska, “Quantitative Analysis and Model Checking,” Proc. 12th IEEE Symp. Logic in Computer Science, pp.111-122, 1997.
[12] D. Kozen, “A Probabilistic PDL,” Proc. 15th ACM Symp. Theory of Computing, pp.291-297, 1983.
[13] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1991.
[14] A. McIver and C. Morgan, “Games, Probability, and the Quantitative $\mu$ -Calculus qM$\mu$ ,” Proc. Int'l Conf. Logic for Programming, Artificial Intelligence, and Reasoning, pp.292-310, 2002.
[15] J.H. Reif, “Universal Games of Incomplete Information,” Proc. 11th Ann. ACM Symp. Theory of Computing, pp.288-308, Apr. 1979.
[16] L.J. Stockmeyer and A.R. Meyer, “Word Problems Requiring Exponential Time,” Proc. Fifth ACM Symp. Theory of Computing, pp.1-9, 1973.
[17] F. van Breugel, “A Behavioural Pseudometric for Metric Labelled Transition Systems,” Proc. 16th Int'l Conf. Concurrency Theory, pp.141-155, 2005.
[18] F. van Breugel and J. Worrel, “An Algorithm for Quantitative Verification of Probabilistic Transition Systems,” Proc. 12th Int'l Conf. Concurrency Theory, pp.336-350, 2001.

Index Terms:
Logic,Extraterrestrial measurements,Cost accounting,Computational modeling,Reasoning about programs,Formal languages,Software tools,Digital audio players,Clocks,Automata,Modal logic,Logics of programs,Specification techniques
"Linear and Branching System Metrics," IEEE Transactions on Software Engineering, vol. 35, no. 2, pp. 1-1, March-April 2009, doi:10.1109/TSE.2008.106
Usage of this product signifies your acceptance of the Terms of Use.