博文
时序逻辑
|||
Contents:
1 时序逻辑程序设计与软件工程 BOOK
2 形式化方法反思： 读《主流之外的经济学家Axel Leijonhufvud》
3 temporal and modal logic, E.Allen Emerson
4 Interval Temporal Logic, Antonio Cau and Ben Moszkowski
5 TEMPORAL LOGIC, Yde Venema
6 Temporal Logic in Information Systems
7
[1] BOOK: 时序逻辑程序设计与软件工程，唐稚松
该书主要介绍唐稚松的基于时序逻辑的XYZ方法。XYZ方法是唐院士20年的心血，是否成功有待时间检验。本文是该书部分内容摘要，从序言、绪论，可以看出唐稚松院士既有豪气，也有怨气。
序
70年代中期之前，计算机科学理论和技术是紧密相联，如形式文法（包括属性文法）及语法分析的研究与变异技术向依存。但自予以形式化问题提出后，由于问题难度大，学者希望寻求新的数学方法和工具加以解决。一部分研究者只注意理论的完美性，如逻辑严密性等因素，却忽略理论的实用性，导致理论与实践脱节。而美国工业界，从实用主义出发，更关心软件生产率、可靠性等关键问题，集中从技术方面入手。两个极端做法作者认为皆不可取，寓意的精确性和技术的自动化两者是不可分割的。
40多年，计算机科学研究实际是围绕某个模型为基础的三层面进行的，即计算机体系、基于该体系的可执行程序语言和表示程序抽象语义的规范语言。例如，主流计算机体系是基于von Neumann模型，则流行程序语言即为适应该体系的命令式语言（如Pascal,C++,Ada等）。von Neumann模型主要特征是自动机状态转换机制，即表现为变量在运行过程中可通过赋值语句改变其值，且其控制流可分解为循环、分支和顺序三种基本结构。其所对应的规范语言是Hoare逻辑的由前置断言与后置断言所表示的逻辑语义。在应用上，基于von Neumann模型的程序语言和规范易学易用。其弱点是自动机状态转换机制不够抽象,包含细节太多(赋值本身即是一种细节)。尤其该机制对于通信进程所组成的并行语义难以表述。故70年代末起，非von Neumann模型研究兴起，特别是函数式模型，包括函数式机器体系、函数式程序语言，以及递归型与函数映射为特征的基于可计算函数（包括λ演算）及代数的语义理论与规范语言等三个层次的研究。从实际应用而言其效果不甚理想。
可见，关键问题在于形式语义理论及规范语言如何研究？
XYZ基于Manna-Pnueli线性时序逻辑。
绪论
程序技术研究30年
过去程序技术研究30年的发展围绕如何提高软件生产率问题。可分为以下三个阶段：一是高级语言阶段，二是结构程序设计阶段，三是软件工程工具阶段。
高级语言阶段
此阶段两大突破：
从Fortran及Algol 60开始设计具有高级控制结构及数据结构易于表示算法的程序语言，即算法语言。
编译技术的成熟
结构程序设计阶段
结构程序语言、面向对象程序设计语言和规范语言。OOL一重要优点是:数据和相关操作封装,从而提高程序可重用性。此外。为了适应某些控制结构复杂的大型反应系统的需要，除了面向领域得以表示静态语义为特征的OOL，更需要一种适应大型同行系统的面向计算得以表示动态语义为特征的程序设计语言或编程环境。
规范语言从程序语言语义的数学理论研究中寻找方法与途径，大致可分为四类：基于可计算函数理论、一阶逻辑、代数、形式文法。四类方法各有千秋。关键问题在于以上语言在目前能不适于表征程序执行的动态语义，难以描述并发程序的语义。
方法论
程序设计方法：
Top-Down：
逐步求精
Bottom-Up：
程序测评方法：
程序验证方法
速成原型法
程序语言转换方法
哲学思路：
合久必分，分久必合
中庸之道
动与静
理想主义和实用主义
中西合璧
个人点评：
我初到武汉读了一会此书，本想借此学习 temporal logic, 感觉太复杂。后来听多名计算机界老师谈到唐稚松院士工作，都认为唐稚松老师在XYZ系统上投入了很大精力，下了大功夫，取得相当成绩，即获得国家自然科学一等奖。但是他们也都认为XYZ系统太复杂了，复杂得令人望而却步。追其原因，唐稚松老师是学哲学和逻辑的，不会编程，没有考虑程序员的需求：简单、好学、好用，比如C。现在唐稚松老师的弟子（包括林院士）几乎都没有延续其工作，原因也在此。
dynamic logic: I don't understand
[2] 形式化方法反思： 读《主流之外的经济学家Axel Leijonhufvud》
Axel Leijonhufvud从20世纪70年代中期起，逐渐从经济学主流中漂移出来。他在1998年说过：
“宏观经济学发生了一个与电影十分类似的转向：即令人目眩神迷的特技越来越多，可是情节简单化的情况也越来越普遍。人们其实盼望出现这样一种宏观经济学，其情节（而不是特技）将给人类状况带来更多的启示。” （见 武夷山老师博文 《主流之外的经济学家Axel Leijonhufvud》）
在某种意义上，形式化方法就是特技。 形式化方法是需要的，就如同维C，但是不能当饭吃。更多时，形式化方法起着锦上添花之用。反之，过犹不及。看过一些论文，明明是很简单的内容，应用了形式化方法，一是概念满天飞，二是定理证明应接不暇。引用我喜欢的一本书《虚拟机的设计与实现 C/C++》
"While I was a graduate student, I learned a dirty little secret about how to get research published. If a professor makes a discovery that can be explained in simple terms, he will go to great lengths and use any number of obfuscation techniques to make the discovery look more complicated than it really is. This is more of a sociological phenomenon than anything else. The train of thought behind this is that if an idea is simple, then it must not be very revolutionary or clever. People who referee journal submissions are more likely to be impressed by an explanation that wraps around itself into a vast Gordian knot.
This may work for professors who want tenure, but it sure doesn't work for software engineers. In his Turing Award lecture, "On Building Systems that will Fail," one of the conclusions Fernando Corbató makes is that sticking to a simple design is necessary for avoiding project failure. You should listen to this man. Corbató is a voice of experience and one of the founding fathers of modern system design. He led the project to build MULTICS back in the 1960s."
过于崇尚形式化的学者多是数学出身，几乎没有编过程序，不知道程序员需要什么？而是一味将数学理论套用于 计算 理论中，也不管是不是适用？一个UML，国内外多少人加形式语义灌水？
学院派：研究在于新，研究一些与众不同的新玩艺，至于有没有用，天知道！关键是在理论层面能够自圆其说。
工程派：开发项目并不追求新奇算法、理论等，但要实用，满足工程指标。
怎么办？A Delicate Balance！How to trade off? This is a question?
3 temporal and modal logic, E.Allen Emerson
Abstract: We give a comprehensive and unifying survey of the theoretical aspects of Temporal and
Modal Logic Note This paper is to appear in the Handbook of Theoretical Computer Science
J van Leeuwen managing editor NorthHolland Pub Co
Modal Logic Note This paper is to appear in the Handbook of Theoretical Computer Science
J van Leeuwen managing editor NorthHolland Pub Co
Temporal and Modal Logic
Based on paper: E.A. Emerson. Temporal and Modal Logic
J. van Leeuwen, editor, Handbook of Theoretical
Computer Science, Volume B: Formal Models and
Semantics, pages 995-1072, Elsevier, 1990
Based on paper: E.A. Emerson. Temporal and Modal Logic
J. van Leeuwen, editor, Handbook of Theoretical
Computer Science, Volume B: Formal Models and
Semantics, pages 995-1072, Elsevier, 1990
4 Interval Temporal Logic
Antonio Cau and Ben Moszkowski: Interval Temporal Logic.pdf
Antonio Cau and Ben Moszkowski: Interval Temporal Logic.pdf
Abstract
Interval Temporal Logic (ITL) is a exible notation for both propositional and
rst-order reasoning about periods of time found in descriptions of hardware and
software systems. Unlike most temporal logics, ITL can handle both sequential
and parallel composition and o ers powerful and extensible speci cation and proof
techniques for reasoning about properties involving safety, liveness and projected
time[15]. Timing constraints are expressible and furthermore most imperative pro-
gramming constructs can be viewed as formulas in a slightly modi ed version of ITL
[25]. Tempura provides an executable framework for developing and experimenting
with suitable ITL speci cations. In addition, ITL and its mature executable subset
Tempura [9] have been extensively used to specify the properties of real-time systems
where the primitive circuits can directly be represented by a set of simple tempo-
ral formulae. In addition, various researchers have applied Tempura to hardware
simulation and other areas where timing is important.
Interval Temporal Logic (ITL) is a exible notation for both propositional and
rst-order reasoning about periods of time found in descriptions of hardware and
software systems. Unlike most temporal logics, ITL can handle both sequential
and parallel composition and o ers powerful and extensible speci cation and proof
techniques for reasoning about properties involving safety, liveness and projected
time[15]. Timing constraints are expressible and furthermore most imperative pro-
gramming constructs can be viewed as formulas in a slightly modi ed version of ITL
[25]. Tempura provides an executable framework for developing and experimenting
with suitable ITL speci cations. In addition, ITL and its mature executable subset
Tempura [9] have been extensively used to specify the properties of real-time systems
where the primitive circuits can directly be represented by a set of simple tempo-
ral formulae. In addition, various researchers have applied Tempura to hardware
simulation and other areas where timing is important.
1 Syntax
5 TEMPORAL LOGIC
Yde Venema
Yde Venema
6 Temporal Logic in Information Systems
Jan Chomicki, David Toman
Abstract
Temporal logic is obtained by adding temporal connectives to
a logic language. Explicit references to time are hidden inside
the temporal connectives. Di erent variants of temporal logic
use di erent sets of such connectives. In this chapter, we survey
the fundamental varieties of temporal logic and describe their
applications in information systems.
Several features of temporal logic make it especially attractive as
a query and integrity constraint language for temporal databases.
First, because the references to time are hidden, queries and integrity
constraints are formulated in an abstract, representationindependent
way. Second, temporal logic is amenable to ecient
implementation. Temporal logic queries can be translated to an
algebraic language. Temporal logic constraints can be eciently
enforced using auxiliary stored information. More general languages,
with explicit references to time, do not share these properties.
Recent research has proposed various implementation techniques
to make temporal logic practically useful in database applications.
Also, the relationships between di erent varieties of temporal
logic and between temporal logic and other temporal languages
have been clari ed. We report on these developments and
outline some of the remaining open research problems.
Temporal logic is obtained by adding temporal connectives to
a logic language. Explicit references to time are hidden inside
the temporal connectives. Di erent variants of temporal logic
use di erent sets of such connectives. In this chapter, we survey
the fundamental varieties of temporal logic and describe their
applications in information systems.
Several features of temporal logic make it especially attractive as
a query and integrity constraint language for temporal databases.
First, because the references to time are hidden, queries and integrity
constraints are formulated in an abstract, representationindependent
way. Second, temporal logic is amenable to ecient
implementation. Temporal logic queries can be translated to an
algebraic language. Temporal logic constraints can be eciently
enforced using auxiliary stored information. More general languages,
with explicit references to time, do not share these properties.
Recent research has proposed various implementation techniques
to make temporal logic practically useful in database applications.
Also, the relationships between di erent varieties of temporal
logic and between temporal logic and other temporal languages
have been clari ed. We report on these developments and
outline some of the remaining open research problems.
https://blog.sciencenet.cn/blog-468147-490086.html
上一篇：review: 马尔可夫逻辑网络研究
下一篇：安全 密码学
扫一扫，分享此博文