Abstract
Often when modelling systems, physical constraints on the resources available are needed. For example, we might say that at most N processes can access a particular resource at any moment or exactly M participants are needed for an agreement. Such situations are concisely modelled where propositions are constrained such that at most N, or exactly M, can hold at any moment in time. This paper describes both the logical basis and a verification method for propositional linear time temporal logics which allow such constraints as input. The method incorporates ideas developed earlier for a resolution method for the temporal logic TLX and a tableaux-like procedure for PTL. The complexity of this procedure is discussed and case studies are examined. The logic itself represents a combination of standard temporal logic with classical constraints restricting the numbers of propositions that can be satisfied at any moment in time.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional Satisfiability and Constraint Programming: A Comparative Survey. ACM Computing Surveys 38(4) (2006)
Chen, B.: Parallel Scheduling for Early Completion. In: Leung, J.Y.-T. (ed.) Handbook of Scheduling: Algorithms, Models, and Performance Analysis, ch. 9, Chapman & Hall/CRC Press (2004)
Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved Automata Generation for Linear Temporal Logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)
Dauzére-Pérès, S., Paulli, J.: An Integrated Approach for Modeling and Solving the General Multiprocessor Job-shop Scheduling Problem using Tabu Search. Annals of Operations Research 70, 281–306 (1997)
Degtyarev, A., Fisher, M., Konev, B.: A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 85–99. Springer, Heidelberg (2002)
Demri, S., Schnoebelen, P.: The Complexity of Propositional Linear Temporal Logic in Simple Cases. Information and Computation 174(1), 84–103 (2002)
Dixon, C., Fisher, M., Konev, B.: Is There a Future for Deductive Temporal Verification? In: Proc. Thirteenth International Symposium on Temporal Representation and Reasoning (TIME), IEEE Computer Society Press, Los Alamitos (2006)
Dixon, C., Fisher, M., Konev, B.: Tractable Temporal Reasoning. In: Proc. International Joint Conference on Artificial Intelligence (IJCAI), AAAI Press, Stanford, California (2007)
Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996–1072. Elsevier, Amsterdam (1990)
Esparza, J.: Decidability and Complexity of Petri Net Problems - An Introduction. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998)
Fisher, M., Dixon, C., Peim, M.: Clausal Temporal Resolution. ACM Transactions on Computational Logic 2(1), 12–56 (2001)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: The Temporal Analysis of Fairness. In: Proc. Seventh ACM Symposium on the Principles of Programming Languages (POPL), pp. 163–173 (January 1980)
Gago, M.-C.F., Hustadt, U., Dixon, C., Fisher, M., Konev, B.: First-Order Temporal Verification in Practice. Journal of Automated Reasoning 34(3), 295–321 (2005)
Giannakopoulou, D., Lerda, F.: From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002)
Gough, G.D.: Decision Procedures for Temporal Logic. Master’s thesis, Department of Computer Science, University of Manchester, October, Also University of Manchester, Department of Computer Science, Technical Report UMCS-89-10-1 (1984)
Jaeger, G., Balsiger, P., Heuerding, A., Schwendimann, S., Bianchi, M., Guggisberg, K., Janssen, G., Heinle, W., Achermann, F., Boroumand, A.D., Brambilla, P., Bucher, I., Zimmermann, H.: LWB–The Logics Workbench 1.1. University of Berne, Switzerland (2002), http://www.lwb.unibe.ch
Janssen, G.: Logics for Digital Circuit Verification: Theory, Algorithms, and Applications. PhD thesis, Eindhoven University of Technology, Eindhoven, The Netherlands (1999)
Kindler, E.: Petri Nets, Situations, and Automata. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 217–236. Springer, Heidelberg (2002)
Kindler, E., Reisig, W., Völzer, H., Walter, R.: Petri Net Based Verification of Distributed Algorithms: An Example. Formal Aspects of Computing 9(4), 409–424 (1997)
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison Wesley Professional, Reading (2003)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)
Schwendimann, S.: Aspects of Computational Logic. PhD thesis, University of Bern, Switzerland (1998)
Sebastiani, R., Tonetta, S., Vardi, M.Y.: Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 350–363. Springer, Heidelberg (2005)
Wolper, P.: The Tableau Method for Temporal Logic: An Overview. Logique et Analyse, 110–111,119–136, (June-September 1985)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dixon, C., Fisher, M., Konev, B. (2007). Temporal Logic with Capacity Constraints. In: Konev, B., Wolter, F. (eds) Frontiers of Combining Systems. FroCoS 2007. Lecture Notes in Computer Science(), vol 4720. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74621-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-74621-8_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74620-1
Online ISBN: 978-3-540-74621-8
eBook Packages: Computer ScienceComputer Science (R0)