×

zbMATH — the first resource for mathematics

Risk assessment for one-counter threads. (English) Zbl 1166.68010
Summary: Threads as contained in a thread algebra are used for the modeling of sequential program behavior. A thread that may use a counter to control its execution is called a ‘one-counter thread’. In this paper the decidability of risk assessment (a certain form of action forecasting) for one-counter threads is proved. This relates to Cohen’s impossibility result on virus detection. Our decidability result follows from a general property of the traces of one-counter threads: if a state is reachable from some initial state, then it is also reachable along a path in which all counter values stay below a fixed bound that depends only on the initial and final counter value. A further consequence is that the reachability of a state is decidable. These properties are based on a result for \(\omega \)-one counter machines by L. E. Rosier and H.-C. Yen [SIAM J. Comput. 16, 779–807 (1987; Zbl 0638.68031)].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bergstra, J.A., Bethke, I.: Polarized process algebra and program equivalence. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) Proceedings of ICALP 2003. Lecture Notes in Comput. Sci., vol. 2719, pp. 1–21. Springer, New York (2003)
[2] Bergstra, J.A., Bethke, I.: Polarized process algebra with reactive composition. Theor. Comput. Sci. 343(3), 285–304 (2005) · Zbl 1077.68057 · doi:10.1016/j.tcs.2005.06.014
[3] Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984) · Zbl 0597.68027 · doi:10.1016/S0019-9958(84)80025-X
[4] Bergstra, J.A., Ponse, A.: Combining programs and state machines. J. Log. Algebr. Program. 51(2), 175–192 (2002) · Zbl 1008.68068 · doi:10.1016/S1567-8326(02)00020-6
[5] Bergstra, J.A., Ponse, A.: A bypass of Cohen’s impossibility result. In: Sloot, P.M.A., Hoekstra, A.G., Priol, T., Reinefeld, A. (eds.) Advances in Grid Computing–EGC 2005. Lecture Notes in Comput. Sci., vol. 3470, pp. 1097–1106. Springer, New York (2005)
[6] Bergstra, J.A., Bethke, I., Ponse, A.: Decision problems for pushdown threads. Acta Inf. 44(2), 75–90 (2007) · Zbl 1120.68077 · doi:10.1007/s00236-007-0040-5
[7] Bergstra, J.A., Bethke, I., Ponse, A.: Thread algebra and risk assessment services. In: Dimitracopoulos, C., et al. (eds.) Logic Colloquium ’05: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Athens, Greece, July 28–August 3, 2005. ASL Lecture Notes in Logic, vol. 28 (to appear) · Zbl 1149.68022
[8] Cohen, F.: Computer viruses–theory and experiments. Comput. Secur. 6(1), 22–35 (1984). Available as http://vx.netlux.org/lib/afc01.html · doi:10.1016/0167-4048(87)90122-2
[9] de Bakker, J.W., Zucker, J.I.: Processes and the denotational semantics of concurrency. Inf. Control 54(1–2), 70–120 (1982) · Zbl 0508.68011 · doi:10.1016/S0019-9958(82)91250-5
[10] Jančar, P., Moller, F., Sawa, Z.: Simulation problems for one-counter machines. In: Proceedings of SOFSEM’99: The 26th Seminar on Current Trends in Theory and Practice of Informatics. Lecture Notes in Comput. Sci., vol. 1725, pp. 398–407. Springer, New York (1999)
[11] Paterson, M.S., Valiant, L.G.: Deterministic one-counter automata. J. Comput. Syst. Sci. 10(3), 340–350 (1975) · Zbl 0307.68038 · doi:10.1016/S0022-0000(75)80005-5
[12] Ponse, A., van der Zwaag, M.B.: An introduction to program and thread algebra. In: Beckmann, A. (ed.) Logical Approaches to Computational Barriers: Proceedings CiE 2006. Lecture Notes in Comput. Sci., vol. 3988, pp. 445–458. Springer, New York (2006) · Zbl 1131.68411
[13] Rosier, L.E., Yen, H.-C.: Logspace hierarchies, polynomial time and the complexity of fairness problems concerning \(\omega\)-machines. SIAM J. Comput. 16(5), 779–807 (1987) · Zbl 0638.68031 · doi:10.1137/0216052
[14] Vu, T.D.: Metric denotational semantics for BPPA. Report PRG0503, Programming Research Group, University of Amsterdam (2005). To appear in J. Log. Algebr. Program.
[15] Yen, H.-C., Yu, L.-P.: Decidability analysis of self-stabilization for infinite state systems. Fundam. Inf. 70(4), 387–402 (2006) · Zbl 1095.68070
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.